commSq — Mathlib

English

The commutative square associated to a bi-Cartesian square in a lattice commutes.

Русский

Связанная квадратная диаграмма для би-картезианского квадрата в решетке коммутирует.

LaTeX

$$$\\mathrm{CommSq}\\big(\\mathrm{homOfLE}(\\mathrm{sq}.le_{12}),\\mathrm{homOfLE}(\\mathrm{sq}.le_{13}),\\mathrm{homOfLE}(\\mathrm{sq}.le_{24}),\\mathrm{homOfLE}(\\mathrm{sq}.le_{34})\\big)$$$

Lean4

/-- The commutative square associated to a bi-Cartesian square in a lattice. -/
theorem commSq : CommSq (homOfLE sq.le₁₂) (homOfLE sq.le₁₃) (homOfLE sq.le₂₄) (homOfLE sq.le₃₄) :=
  ⟨rfl⟩

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