comap_inf — Mathlib

English

The comap of the infimum equals the infimum of comaps: (L ⊓ M).comap f = L.comap f ⊓ M.comap f.

Русский

Обратное образование пересечения равно пересечению обратных образований: (L ⊓ M).comap f = L.comap f ⊓ M.comap f.

LaTeX

$$$ (L \sqcap M).comap f = L.comap f \sqcap M.comap f $$$

Lean4

theorem comap_inf (L M : BooleanSubalgebra β) (f : BoundedLatticeHom α β) : (L ⊓ M).comap f = L.comap f ⊓ M.comap f :=
  (gc_map_comap f).u_inf

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