coe_consEquiv_of_eq_of_lt — Mathlib

English

If x.fst = v and x.snd.val < m.count v, then consEquiv x = some ⟨x.fst, ⟨x.snd.val, … ⟩⟩.

Русский

Если x.fst = v и x.snd.val < m.count v, то consEquiv x = some ⟨x.fst, ⟨x.snd.val, … ⟩⟩.

LaTeX

$$$ \text{coe\_consEquiv\_of\_eq\_of\_lt}(x) : consEquiv x = \mathrm{Some}(\langle x.fst, \langle x.snd.val, \dots \rangle \rangle) $$$

Lean4

theorem coe_consEquiv_of_eq_of_lt {v : α} (x : v ::ₘ m) (hx : ↑x = v) (hx2 : x.2 < m.count v) :
    consEquiv x = some ⟨x.1, ⟨x.2, by simpa [hx]⟩⟩ := by simp [consEquiv, hx, hx2.ne]

Похожие утверждения