finsetSup'_mem — Mathlib

English

If s is SupClosed and t is a nonempty Finset, and f(i) ∈ s for all i ∈ t, then the Finset.sup' t f belongs to s.

Русский

Пусть s замкнуто по ⊔ и t непустой Finset; если для всех i ∈ t выполняется f(i) ∈ s, то t.sup' f ∈ s.

LaTeX

$$$ (\\forall i \\in t, f(i) \\in s) \\Rightarrow t.sup' ht f \\in s $$$

Lean4

theorem finsetSup'_mem (hs : SupClosed s) (ht : t.Nonempty) : (∀ i ∈ t, f i ∈ s) → t.sup' ht f ∈ s :=
  sup'_induction _ _ hs

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