comp_sup'_eq_sup'_comp — Mathlib

English

If g preserves sup, then g(s.sup' f) = s.sup' (g ∘ f).

Русский

Если g сохраняет супремум, то applying g к sup' f равен sup' (g∘f).

LaTeX

$$$g(s.sup' H f) = s.sup' H (g \circ f)$$$

Lean4

theorem comp_sup'_eq_sup'_comp [SemilatticeSup γ] {s : Finset β} (H : s.Nonempty) {f : β → α} (g : α → γ)
    (g_sup : ∀ x y, g (x ⊔ y) = g x ⊔ g y) : g (s.sup' H f) = s.sup' H (g ∘ f) := by
  refine H.cons_induction ?_ ?_ <;> intros <;> simp [*]

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