comp_sup_eq_sup_comp_of_is_total — Mathlib

English

If g is a monotone map between lattices that preserves bottom and the target lattice is a semilattice with top, then g preserves finite suprema: g(sup f) = sup (g ∘ f).

Русский

Пусть g монотонна и отображает нижний элемент в нижний; тогда она сохраняет конечные супремумы: g( sup f ) = sup (g ∘ f).

LaTeX

$$$g(\sup f) = \sup (g \circ f)$, при монотонности g и $g(\bot)=\bot$$$

Lean4

theorem comp_sup_eq_sup_comp_of_is_total [SemilatticeSup β] [OrderBot β] (g : α → β) (mono_g : Monotone g)
    (bot : g ⊥ = ⊥) : g (s.sup f) = s.sup (g ∘ f) :=
  comp_sup_eq_sup_comp g mono_g.map_sup bot

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