inrX_sndX — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem inrX_sndX (i : ι) : inrX φ i ≫ sndX φ i = 𝟙 _ :=
  by
  dsimp [sndX, inrX]
  split_ifs with hi <;> simp

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