sndX_inrX — Mathlib

English

For every i, sndX φ i followed by inrX φ i is the identity on X φ i.

Русский

Для каждого i композиция sndX φ i ∘ inrX φ i равна тождественному морфизму на X φ i.

LaTeX

$$$ sndX\\,\\phi\\,i \\;\\circ\\; inrX\\,\\phi\\,i = \\mathrm{id}_{X\\,\\phi\\,i}. $$$

Lean4

@[reassoc]
theorem sndX_inrX (i : ι) (hi : ¬c.Rel i (c.next i)) : sndX φ i ≫ inrX φ i = 𝟙 _ :=
  by
  dsimp [sndX, inrX]
  simp only [dif_neg hi, Iso.hom_inv_id]

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