inf'_apply — Mathlib

English

For nonempty finite set s and f: ι → C(α, β), (s.inf' H f) a = s.inf' H (λ i, f(i) a).

Русский

Для непустого конечного множества s и f: ι → C(α, β): (s.inf' H f) a = s.inf' H (λ i, f(i) a).

LaTeX

$$For H : s.Nonempty, (s.inf' H f) a = s.inf' H (λ i, f(i) a).$$

Lean4

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

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