Documentation Verification Report

Basic

📁 Source: PhysLean/Relativity/Tensors/RealTensor/Velocity/Basic.lean

Statistics

Metric	Count
Definitions `instTopologicalSpaceElemVector`, `instZeroElemVector`, `pathFromZero`, `zero`	4
Theorems `ext`, `ext_iff`, `isPathConnected`, `mem_iff`, `minkowskiProduct_continuous_fst`, `minkowskiProduct_continuous_snd`, `minkowskiProduct_self_eq_one`, `norm_spatialPart_le_timeComponent`, `norm_spatialPart_sq_eq`, `one_add_minkowskiProduct_neq_zero`, `timeComponent_abs`, `timeComponent_nonneg`, `timeComponent_pos`, `zero_le_minkowskiProduct`, `zero_timeComponent`	15
Total	19

Lorentz.Velocity

Definitions

Name	Category	Theorems
`instTopologicalSpaceElemVector` 📖	CompOp	6 math math: `minkowskiProduct_continuous_fst`, `LorentzGroup.toVelocity_continuous`, `minkowskiProduct_continuous_snd`, `LorentzGroup.generalizedBoost_continuous_snd`, `isPathConnected`, `LorentzGroup.generalizedBoost_continuous_fst`
`instZeroElemVector` 📖	CompOp	1 math math: `zero_timeComponent`
`pathFromZero` 📖	CompOp	—
`zero` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`Lorentz.Vector` `Lorentz.Velocity`	—	—	—
`ext_iff` 📖	mathematical	—	`Lorentz.Vector` `Lorentz.Velocity`	—	`ext`
`isPathConnected` 📖	mathematical	—	`Lorentz.Vector` `Lorentz.Velocity` `instTopologicalSpaceElemVector`	—	—
`mem_iff` 📖	mathematical	—	`Lorentz.Vector` `Lorentz.Velocity` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.minkowskiProduct` `Lorentz.Vector.timeComponent`	—	—
`minkowskiProduct_continuous_fst` 📖	mathematical	—	`Lorentz.Vector` `Lorentz.Velocity` `instTopologicalSpaceElemVector` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.minkowskiProduct`	—	`Lorentz.Vector.minkowskiProduct_symm` `minkowskiProduct_continuous_snd`
`minkowskiProduct_continuous_snd` 📖	mathematical	—	`Lorentz.Vector` `Lorentz.Velocity` `instTopologicalSpaceElemVector` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.minkowskiProduct`	—	—
`minkowskiProduct_self_eq_one` 📖	mathematical	—	`Lorentz.Vector` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.minkowskiProduct` `Lorentz.Velocity`	—	—
`norm_spatialPart_le_timeComponent` 📖	mathematical	—	`Lorentz.Vector.spatialPart` `Lorentz.Vector` `Lorentz.Velocity` `Lorentz.Vector.timeComponent`	—	`minkowskiProduct_self_eq_one` `Lorentz.Vector.minkowskiProduct_self_eq_timeComponent_spatialPart` `timeComponent_abs`
`norm_spatialPart_sq_eq` 📖	mathematical	—	`Lorentz.Vector.spatialPart` `Lorentz.Vector` `Lorentz.Velocity`	—	`minkowskiProduct_self_eq_one` `Lorentz.Vector.minkowskiProduct_self_eq_timeComponent_spatialPart` `timeComponent_abs`
`one_add_minkowskiProduct_neq_zero` 📖	—	—	—	—	`zero_le_minkowskiProduct`
`timeComponent_abs` 📖	mathematical	—	`Lorentz.Vector.timeComponent` `Lorentz.Vector` `Lorentz.Velocity`	—	—
`timeComponent_nonneg` 📖	mathematical	—	`Lorentz.Vector.timeComponent` `Lorentz.Vector` `Lorentz.Velocity`	—	`timeComponent_pos`
`timeComponent_pos` 📖	mathematical	—	`Lorentz.Vector.timeComponent` `Lorentz.Vector` `Lorentz.Velocity`	—	—
`zero_le_minkowskiProduct` 📖	mathematical	—	`Lorentz.Vector` `Lorentz.Vector.isNormedAddCommGroup` `Lorentz.Vector.instAddCommMonoid` `Lorentz.Vector.instModuleReal` `Lorentz.Vector.instAddCommGroup` `Lorentz.Vector.minkowskiProduct` `Lorentz.Velocity`	—	`norm_spatialPart_le_timeComponent` `Lorentz.Vector.minkowskiProduct_eq_timeComponent_spatialPart` `timeComponent_abs`
`zero_timeComponent` 📖	mathematical	—	`Lorentz.Vector.timeComponent` `Lorentz.Vector` `Lorentz.Velocity` `instZeroElemVector`	—	`Lorentz.Vector.basis_apply`

---

← Back to Index