Basic

📁 Source: PhysLean/Relativity/LorentzGroup/Orthochronous/Basic.lean

Statistics

Metric	Count
Definitions `IsOrthochronous`, `orthchroMap`, `orthchroMapReal`, `orthchroRep`, `orthochronoustoVelocity`, `stepFunction`, `timeCompCont`	7
Theorems `iff_in_orthchroRep_ker`, `id_isOrthochronous`, `isOrthochronous_iff_ge_one`, `isOrthochronous_iff_not_neg`, `isOrthochronous_iff_of_orthchroMap_eq`, `isOrthochronous_iff_toVector_timeComponet_nonneg`, `isOrthochronous_iff_transpose`, `isOrthochronous_inv_iff`, `isOrthochronous_mul`, `isOrthochronous_mul_iff`, `isOrthochronous_on_connected_component`, `neg_isOrthochronous_iff_not`, `not_isOrthochronous_iff_le_neg_one`, `not_isOrthochronous_iff_le_zero`, `not_isOrthochronous_iff_toVector_timeComponet_nonpos`, `orthchroMapReal_minus_one_or_one`, `orthchroMapReal_on_IsOrthochronous`, `orthchroMapReal_on_not_IsOrthochronous`, `orthchroMap_IsOrthochronous`, `orthchroMap_not_IsOrthochronous`, `orthchroRep_inv_eq_self`, `stepFunction_continuous`	22
Total	29

LorentzGroup

Definitions

Name	Category	Theorems
`IsOrthochronous` 📖	MathDef	18 math math: `isOrthochronous_iff_not_neg`, `generalizedBoost_isOrthochronous`, `not_isOrthochronous_iff_toVector_timeComponet_nonpos`, `isOrthochronous_iff_transpose`, `IsOrthochronous.iff_in_orthchroRep_ker`, `isOrthochronous_on_connected_component`, `lorentzAlgebra.exp_isOrthochronous`, `isOrthochronous_iff_of_orthchroMap_eq`, `isOrthochronous_inv_iff`, `isOrthochronous_of_restricted`, `not_isOrthochronous_iff_le_neg_one`, `Lorentz.SL2C.toLorentzGroup_isOrthochronous`, `isOrthochronous_iff_ge_one`, `id_isOrthochronous`, `not_isOrthochronous_iff_le_zero`, `isOrthochronous_mul_iff`, `isOrthochronous_iff_toVector_timeComponet_nonneg`, `neg_isOrthochronous_iff_not`
`orthchroMap` 📖	CompOp	2 math math: `orthchroMap_not_IsOrthochronous`, `orthchroMap_IsOrthochronous`
`orthchroMapReal` 📖	CompOp	3 math math: `orthchroMapReal_minus_one_or_one`, `orthchroMapReal_on_not_IsOrthochronous`, `orthchroMapReal_on_IsOrthochronous`
`orthchroRep` 📖	CompOp	2 math math: `IsOrthochronous.iff_in_orthchroRep_ker`, `orthchroRep_inv_eq_self`
`orthochronoustoVelocity` 📖	CompOp	—
`stepFunction` 📖	CompOp	1 math math: `stepFunction_continuous`
`timeCompCont` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`id_isOrthochronous` 📖	mathematical	—	`IsOrthochronous` `LorentzGroup` `lorentzGroupIsGroup`	—	—
`isOrthochronous_iff_ge_one` 📖	mathematical	—	`IsOrthochronous` `LorentzGroup`	—	`one_le_abs_timeComponent`
`isOrthochronous_iff_not_neg` 📖	mathematical	—	`IsOrthochronous` `LorentzGroup` `instNegElemMatrixSumFinOfNatNatReal`	—	`not_isOrthochronous_iff_le_neg_one` `isOrthochronous_iff_ge_one`
`isOrthochronous_iff_of_orthchroMap_eq` 📖	mathematical	`LorentzGroup` `instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup` `instTopologicalSpaceMultiplicativeZModOfNatNat` `orthchroMap`	`IsOrthochronous`	—	`IsOrthochronous.iff_in_orthchroRep_ker`
`isOrthochronous_iff_toVector_timeComponet_nonneg` 📖	mathematical	—	`IsOrthochronous` `Lorentz.Vector.timeComponent` `toVector`	—	`toVector_apply`
`isOrthochronous_iff_transpose` 📖	mathematical	—	`IsOrthochronous` `transpose`	—	—
`isOrthochronous_inv_iff` 📖	mathematical	—	`IsOrthochronous` `LorentzGroup` `lorentzGroupIsGroup`	—	`dual_mem` `inv_eq_dual` `minkowskiMatrix.dual_apply` `minkowskiMatrix.inl_0_inl_0`
`isOrthochronous_mul` 📖	mathematical	`IsOrthochronous`	`LorentzGroup` `lorentzGroupIsGroup`	—	`isOrthochronous_iff_toVector_timeComponet_nonneg` `toVector_mul` `smul_timeComponent_eq_toVector_minkowskiProduct` `Lorentz.Velocity.zero_le_minkowskiProduct` `isOrthochronous_inv_iff`
`isOrthochronous_mul_iff` 📖	mathematical	—	`IsOrthochronous` `LorentzGroup` `lorentzGroupIsGroup`	—	`isOrthochronous_iff_toVector_timeComponet_nonneg` `toVector_mul` `smul_timeComponent_eq_toVector_minkowskiProduct` `isOrthochronous_inv_iff` `Lorentz.Velocity.zero_le_minkowskiProduct` `not_isOrthochronous_iff_toVector_timeComponet_nonpos` `neg_isOrthochronous_iff_not` `toVector_neg` `inv_neg`
`isOrthochronous_on_connected_component` 📖	mathematical	`LorentzGroup` `instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup`	`IsOrthochronous`	—	`instDiscreteTopologyMultiplicativeZModOfNatNat` `isOrthochronous_iff_of_orthchroMap_eq`
`neg_isOrthochronous_iff_not` 📖	mathematical	—	`IsOrthochronous` `LorentzGroup` `instNegElemMatrixSumFinOfNatNatReal`	—	`isOrthochronous_iff_not_neg`
`not_isOrthochronous_iff_le_neg_one` 📖	mathematical	—	`IsOrthochronous` `LorentzGroup`	—	`one_le_abs_timeComponent`
`not_isOrthochronous_iff_le_zero` 📖	mathematical	—	`IsOrthochronous` `LorentzGroup`	—	`one_le_abs_timeComponent`
`not_isOrthochronous_iff_toVector_timeComponet_nonpos` 📖	mathematical	—	`IsOrthochronous` `Lorentz.Vector.timeComponent` `toVector`	—	`not_isOrthochronous_iff_le_zero` `toVector_apply`
`orthchroMapReal_minus_one_or_one` 📖	mathematical	—	`LorentzGroup` `instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup` `orthchroMapReal`	—	`orthchroMapReal_on_IsOrthochronous` `orthchroMapReal_on_not_IsOrthochronous`
`orthchroMapReal_on_IsOrthochronous` 📖	mathematical	`IsOrthochronous`	`LorentzGroup` `instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup` `orthchroMapReal`	—	`stepFunction.eq_1` `isOrthochronous_iff_ge_one`
`orthchroMapReal_on_not_IsOrthochronous` 📖	mathematical	`IsOrthochronous`	`LorentzGroup` `instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup` `orthchroMapReal`	—	`stepFunction.eq_1` `not_isOrthochronous_iff_le_neg_one`
`orthchroMap_IsOrthochronous` 📖	mathematical	`IsOrthochronous`	`LorentzGroup` `instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup` `instTopologicalSpaceMultiplicativeZModOfNatNat` `orthchroMap`	—	`orthchroMapReal_minus_one_or_one` `orthchroMapReal_on_IsOrthochronous`
`orthchroMap_not_IsOrthochronous` 📖	mathematical	`IsOrthochronous`	`LorentzGroup` `instTopologicalSpaceElemMatrixSumFinOfNatNatRealLorentzGroup` `instTopologicalSpaceMultiplicativeZModOfNatNat` `orthchroMap`	—	`orthchroMapReal_minus_one_or_one` `orthchroMapReal_on_not_IsOrthochronous`
`orthchroRep_inv_eq_self` 📖	mathematical	—	`LorentzGroup` `lorentzGroupIsGroup` `orthchroRep`	—	`orthchroMap_IsOrthochronous` `orthchroMap_not_IsOrthochronous`
`stepFunction_continuous` 📖	mathematical	—	`stepFunction`	—	—

LorentzGroup.IsOrthochronous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iff_in_orthchroRep_ker` 📖	mathematical	—	`LorentzGroup.IsOrthochronous` `LorentzGroup` `lorentzGroupIsGroup` `LorentzGroup.orthchroRep`	—	`LorentzGroup.orthchroMap_IsOrthochronous` `LorentzGroup.orthchroMap_not_IsOrthochronous`

---

← Back to Index