commSq — Mathlib

English

For isHomLift data, the square formed by p.map φ and the domain/codomain equalities commutes; i.e. the constructed square is a commutative square.

Русский

Для данных IsHomLift квадрат, составленный из p.map φ и равенств домена/кодрома, коммутирует.

LaTeX

$$$CommSq\\ (p.map\\ \\phi)\\ (eqToHom(\\mathrm{domain\_eq}\\ p\\ f\\ φ))\\ (eqToHom(\\mathrm{codomain\\_eq}\\ p\\ f\\ φ))\\ f$$$

Lean4

theorem commSq : CommSq (p.map φ) (eqToHom (domain_eq p f φ)) (eqToHom (codomain_eq p f φ)) f where
  w := by simp only [fac p f φ, eqToHom_trans_assoc, eqToHom_refl, id_comp]

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