map_finset_sup — Mathlib

English

If f is a suitable functor-like map, then f(s.sup g) = s.sup (f ∘ g).

Русский

Если отображение f совместимо с операцией свёртки, то f(s.sup g) = s.sup (f ∘ g).

LaTeX

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

Lean4

@[simp]
theorem _root_.map_finset_sup [SemilatticeSup β] [OrderBot β] [FunLike F α β] [SupBotHomClass F α β] (f : F)
    (s : Finset ι) (g : ι → α) : f (s.sup g) = s.sup (f ∘ g) :=
  Finset.cons_induction_on s (map_bot f) fun i s _ h => by rw [sup_cons, sup_cons, map_sup, h, Function.comp_apply]

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