iSup_mem — Mathlib

English

If the bottom element belongs to s and every f(i) ∈ s for all i, then iSup f(i) ∈ s.

Русский

Если ⊥ ∈ s и все f(i) ∈ s, то iSup f(i) ∈ s.

LaTeX

$$$[Finite ι] \\Rightarrow [⊥ ∈ s] ∧ (\\forall i, f(i) ∈ s) \\Rightarrow (\\\\bigvee_i f(i) ∈ s).$$$

Lean4

theorem iSup_mem [Finite ι] (hs : SupClosed s) (hbot : ⊥ ∈ s) (hf : ∀ i, f i ∈ s) : ⨆ i, f i ∈ s :=
  by
  cases isEmpty_or_nonempty ι
  · simpa [iSup_of_empty]
  · exact hs.iSup_mem_of_nonempty hf

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