inlX_fstX — Mathlib

English

For all i, j with hij, the composition inlX φ i j hij followed by fstX φ j i hij is the identity on F.X i.

Русский

Для любых i, j с hij, композиция inlX φ i j hij ∘ fstX φ j i hij равна тождественному морфизму на F.X i.

LaTeX

$$$ inlX\\,\\phi\\,i\\,j\\,hij \\;\\circ\\; fstX\\,\\phi\\,j\\,i\\,hij = \\mathrm{id}_{F.X_i}. $$$

Lean4

@[reassoc (attr := simp)]
theorem inlX_fstX (i j : ι) (hij : c.Rel j i) : inlX φ i j hij ≫ fstX φ j i hij = 𝟙 _ := by simp [inlX, fstX]

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