finsetInf_mem — Mathlib

English

Assume α has a top element. If s is InfClosed and t is a nonempty Finset, and f(i) ∈ s for all i ∈ t, then t.inf f ∈ s.

Русский

Пусть у α есть верхняя граница. Если s InfClosed, t — непустой Finset, и для всех i ∈ t имеются f(i) ∈ s, тогда t.inf f ∈ s.

LaTeX

$$$[OrderTop\\ \\alpha] \\ (hs : InfClosed\\ s)\\ (ht : t.Nonempty) → (\\forall i ∈ t, f\\ i ∈ s) → t.inf\\ f ∈ s$$$

Lean4

theorem finsetInf_mem [OrderTop α] (hs : InfClosed s) (ht : t.Nonempty) : (∀ i ∈ t, f i ∈ s) → t.inf f ∈ s :=
  inf'_eq_inf ht f ▸ hs.finsetInf'_mem ht

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