inf_attach — Mathlib

English

For any Finset s of β and function f: β → α, the infimum over the attached elements equals the infimum over s: (s.attach inf (λ x, f x)) = s.inf f.

Русский

Для конечного множества s над β и функции f: β → α верно: (s.attach).inf (λ x, f x) = s.inf f.

LaTeX

$$$ (s.attach).inf (\\\\lambda x, f x) = s.inf f $$$

Lean4

theorem inf_attach (s : Finset β) (f : β → α) : (s.attach.inf fun x => f x) = s.inf f :=
  @sup_attach αᵒᵈ _ _ _ _ _

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