le_comap_sup — Mathlib

English

comap preserves supremum: comap f K ⊔ comap f L ≤ comap f (K ⊔ L).

Русский

прообраз сохраняет верхнюю грань: comap f K ⊔ comap f L ≤ comap f (K ⊔ L).

LaTeX

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

Lean4

theorem le_comap_sup : comap f K ⊔ comap f L ≤ comap f (K ⊔ L) :=
  (gc_map_comap f : GaloisConnection (map f) (comap f)).monotone_u.le_map_sup _
    _
      -- TODO: Should these be simp lemmas?

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