sigma_eq_iff_eq_comp_cast — Mathlib

English

Equality in a dependent sigma type is equivalent to the existence of a cast h such that the second components are related by composition with Fin.cast.

Русский

Равенство в зависимом сигма-типе эквивалентно существованию отображения через Fin.cast так, что вторые компоненты связаны комбинацией.

LaTeX

$$$a = b \\;\\iff\\; \\exists h, a.fst = b.fst \\land a.snd = b.snd \\circ Fin.cast h$$$

Lean4

/-- `Fin.sigma_eq_of_eq_comp_cast` as an `iff`. -/
theorem sigma_eq_iff_eq_comp_cast {α : Type*} {a b : Σ ii, Fin ii → α} :
    a = b ↔ ∃ h : a.fst = b.fst, a.snd = b.snd ∘ Fin.cast h :=
  ⟨fun h ↦ h ▸ ⟨rfl, funext <| Fin.rec fun _ _ ↦ rfl⟩, fun ⟨_, h'⟩ ↦ sigma_eq_of_eq_comp_cast _ h'⟩

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