def
definition
tickSucc
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.TimeAsOrbit on GitHub at line 47.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
44/-! ## The Tick Successor -/
45
46/-- The canonical successor on `Tick`: advance the index by one. -/
47def tickSucc (t : Tick) : Tick := ⟨t.index + 1⟩
48
49@[simp] theorem tickSucc_index (t : Tick) : (tickSucc t).index = t.index + 1 := rfl
50
51/-- The canonical zero tick. -/
52def tickZero : Tick := ⟨0⟩
53
54@[simp] theorem tickZero_index : tickZero.index = 0 := rfl
55
56/-! ## Tick is canonically the natural numbers -/
57
58/-- The canonical equivalence between `Tick` and `Nat` via the index. -/
59def tickEquivNat : Tick ≃ Nat where
60 toFun t := t.index
61 invFun n := ⟨n⟩
62 left_inv := by intro t; cases t; rfl
63 right_inv := by intro n; rfl
64
65@[simp] theorem tickEquivNat_apply (t : Tick) : tickEquivNat t = t.index := rfl
66@[simp] theorem tickEquivNat_symm_apply (n : Nat) :
67 tickEquivNat.symm n = ⟨n⟩ := rfl
68
69@[simp] theorem tickEquivNat_zero : tickEquivNat tickZero = 0 := rfl
70
71@[simp] theorem tickEquivNat_succ (t : Tick) :
72 tickEquivNat (tickSucc t) = (tickEquivNat t) + 1 := rfl
73
74/-- The canonical equivalence `Tick ≃ LogicNat` via `Nat`. -/
75def tickEquivLogicNat : Tick ≃ LogicNat :=
76 tickEquivNat.trans LogicNat.equivNat.symm
77