comp_sup_eq_sup_comp_of_nonempty — Mathlib

English

Let g be monotone and s be nonempty; then g(sup f) = sup(g ∘ f).

Русский

Пусть g монотонна и s непусто; тогда g( sup f ) = sup (g ∘ f).

LaTeX

$$$\text{monotone}(g) \; \Rightarrow\; g\bigl(\,s^{\uparrow} f\bigr) = s^{\uparrow} (g \circ f).$$$

Lean4

theorem comp_sup_eq_sup_comp_of_nonempty [OrderBot α] [SemilatticeSup β] [OrderBot β] {g : α → β} (mono_g : Monotone g)
    (H : s.Nonempty) : g (s.sup f) = s.sup (g ∘ f) :=
  by
  rw [← Finset.sup'_eq_sup H, ← Finset.sup'_eq_sup H]
  exact Finset.comp_sup'_eq_sup'_comp H g (fun x y ↦ Monotone.map_sup mono_g x y)

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