comp_sup_eq_sup_comp — Mathlib

English

If g preserves finite joins and maps ⊥ to ⊥, then g distributes over finite suprema: g(sup f) = sup(g ∘ f).

Русский

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

LaTeX

$$$\displaystyle g (s.\sup f) = s.\sup (g \circ f)$$$

Lean4

theorem comp_sup_eq_sup_comp [SemilatticeSup γ] [OrderBot γ] {s : Finset β} {f : β → α} (g : α → γ)
    (g_sup : ∀ x y, g (x ⊔ y) = g x ⊔ g y) (bot : g ⊥ = ⊥) : g (s.sup f) = s.sup (g ∘ f) :=
  Finset.cons_induction_on s bot fun c t hc ih => by rw [sup_cons, sup_cons, g_sup, ih, Function.comp_apply]

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