ProperTime

📁 Source: PhysLean/Relativity/Special/ProperTime.lean

Statistics

Metric	Count
Definitions properTime	1
Theorems properTime_pos_ofTimeLike, properTime_zero_ofLightLike, properTime_zero_ofSpaceLike	3
Total	4

SpaceTime

Definitions

Name	Category	Theorems
properTime 📖	CompOp	3 math math: properTime_pos_ofTimeLike, properTime_zero_ofSpaceLike, properTime_zero_ofLightLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
properTime_pos_ofTimeLike 📖	mathematical	Lorentz.Vector.causalCharacter SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.CausalCharacter.timeLike	properTime	—	properTime.eq_1 Lorentz.Vector.timeLike_iff_norm_sq_pos
properTime_zero_ofLightLike 📖	mathematical	Lorentz.Vector.causalCharacter SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.CausalCharacter.lightLike	properTime	—	properTime.eq_1 Lorentz.Vector.lightLike_iff_norm_sq_zero
properTime_zero_ofSpaceLike 📖	mathematical	Lorentz.Vector.causalCharacter SpaceTime Lorentz.Vector.isNormedAddCommGroup Lorentz.Vector.CausalCharacter.spaceLike	properTime	—	properTime.eq_1 Lorentz.Vector.spaceLike_iff_norm_sq_neg

---

← Back to Index