consEquiv_symm_some — Mathlib

English

The inverse image of some x under consEquiv is the pair ⟨x.fst, x.snd.castLE(… )⟩.

Русский

Обратное изображение некоторого x под consEquiv — пара ⟨x.fst, x.snd.castLE(… )⟩.

LaTeX

$$$ (consEquiv (v := v)).\mathrm{symm} (\mathrm{Some}(x)) = \langle x.\mathrm{fst}, x.\mathrm{snd}.castLE(\dots) \rangle $$$

Lean4

@[simp]
theorem consEquiv_symm_some {v : α} {x : m} :
    (consEquiv (v := v)).symm (some x) = ⟨x, x.2.castLE (count_le_count_cons ..)⟩ :=
  rfl

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