sup'_apply — Mathlib

English

For a nonempty Finset s and a family f of continuous maps, the pointwise sup' over s equals the sup' over the evaluations: (s.sup' H f) a = s.sup' H (λ i, f i a).

Русский

Для непустого множества Finset s и семейства отображений f выполняется равенство точки-wise: (s.sup' H f) a = s.sup' H (λ i, f i a).

LaTeX

$$$s.sup' H f\\, a = s.sup' H (\\lambda i. f(i)\\, a)$.$$

Lean4

theorem sup'_apply {ι : Type*} {s : Finset ι} (H : s.Nonempty) (f : ι → C(α, β)) (a : α) :
    s.sup' H f a = s.sup' H fun i ↦ f i a :=
  Finset.comp_sup'_eq_sup'_comp H (fun g : C(α, β) ↦ g a) fun _ _ ↦ rfl

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