finsetSup_mem — Mathlib

English

In an order with bottom, if s is SupClosed and t is nonempty, and f(i) ∈ s for all i in t, then the Finset.sup f over t is in s.

Русский

В порядке с нулём, если s замкнуто по ⊔ и t не пуст, и f(i) ∈ s для всех i ∈ t, то t.sup f ∈ s.

LaTeX

$$$ [OrderBot \\alpha] (\\forall i \\in t, f(i) \\in s) \\Rightarrow t.sup f \\in s $$$

Lean4

theorem finsetSup_mem [OrderBot α] (hs : SupClosed s) (ht : t.Nonempty) : (∀ i ∈ t, f i ∈ s) → t.sup f ∈ s :=
  sup'_eq_sup ht f ▸ hs.finsetSup'_mem ht

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