map_finset_sup' — Mathlib

English

For a FunLike f and SupHomClass, the map of a Finset's sup' equals the sup' of the mapped elements.

Русский

Для отображения, сохраняющего супремум, отображение картинки над Finset сохраняет sup'.

LaTeX

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

Lean4

@[simp]
theorem _root_.map_finset_sup' [SemilatticeSup β] [FunLike F α β] [SupHomClass F α β] (f : F) {s : Finset ι} (hs)
    (g : ι → α) : f (s.sup' hs g) = s.sup' hs (f ∘ g) := by refine hs.cons_induction ?_ ?_ <;> intros <;> simp [*]

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