le_comap_sup — Mathlib

English

The comap of a join dominates the join of comaps: comap f L ⊔ comap f M ≤ comap f (L ⊔ M).

Русский

Обратное образование объединения доминирует над объединением обратных образований: comap f L ⊔ comap f M ≤ comap f (L ⊔ M).

LaTeX

$$$\operatorname{comap} f L \sqcup \operatorname{comap} f M \le \operatorname{comap} f (L \sqcup M)$$$

Lean4

theorem le_comap_sup (L M : BooleanSubalgebra β) (f : BoundedLatticeHom α β) :
    comap f L ⊔ comap f M ≤ comap f (L ⊔ M) :=
  comap_mono.le_map_sup _ _

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