ι_flip — Mathlib

English

Two variants of the flip equality for PushoutObjObj hold; flipping the square preserves the equality of the injection maps.

Русский

Сохранение равенства при развороте квадрата в PushoutObjObj: ι_flip равен ι.

LaTeX

$$$\\text{sq.flip.ι} = \\text{sq.ι}$$$

Lean4

@[simp]
theorem ι_flip : sq.flip.ι = sq.ι := by
  apply sq.flip.isPushout.hom_ext
  · rw [inl_ι, flip_inl, inr_ι, flip_obj_map]
  · rw [inr_ι, flip_inr, inl_ι, flip_map_app]

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