le_comap_iSup — Mathlib

English

The join of comaps is below the comap of the join: ⨆ i, (L i).comap f ≤ (⨆ i, L i).comap f.

Русский

Сложение обратных образований ниже обратного образа сложения: ⨆ i, (L_i).comap f ≤ (⨆ i, L_i).comap f.

LaTeX

$$$\bigvee_i (L_i.\mathrm{comap} f) \le (\bigvee_i L_i).\mathrm{comap} f$$$

Lean4

theorem le_comap_iSup (f : BoundedLatticeHom α β) (L : ι → BooleanSubalgebra β) :
    ⨆ i, (L i).comap f ≤ (⨆ i, L i).comap f :=
  comap_mono.le_map_iSup

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