DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Update FourVelocity.lean

Browse source
This commit is contained in:
Pietro Monticone 2024-06-08 01:52:44 +02:00
parent c608d8c289
commit e6bea53658
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/SpaceTime/FourVelocity.lean
View file

@ -70,7 +70,7 @@ lemma zero_nonneg_iff (v : PreFourVelocity) : 0 ≤ v.1 0 ↔ 1 ≤ v.1 0 := by
· intro h
linarith
/-- A `PreFourVelocity` is a `FourVelocity` if its time componenet is non-negative. -/
/-- A `PreFourVelocity` is a `FourVelocity` if its time component is non-negative. -/
def IsFourVelocity (v : PreFourVelocity) : Prop := 0 ≤ v.1 0