theorem
proved
decidable or rfl
time_before_spacetime
show as:
view Lean formalization →
formal statement (Lean)
101theorem time_before_spacetime :
102 Before Stage.timeTick Stage.spacetime := by
proof body
Decided by rfl or decide.
103 decide
104