isUpperSet_sUnion — Mathlib

English

If S is a set of upper sets and every member s ∈ S is an upper set, then the union of S is upper.

Русский

Если S — множество верхних множеств и каждый элемент s ∈ S является верхним множеством, то объединение S — верхнее множество.

LaTeX

$$$\forall S. (S \subseteq \mathcal{P}(\alpha) \text{ and } \text{∀} s ∈ S, IsUpperSet(s)) \Rightarrow IsUpperSet(\bigcup S)$$$

Lean4

theorem isUpperSet_sUnion {S : Set (Set α)} (hf : ∀ s ∈ S, IsUpperSet s) : IsUpperSet (⋃₀ S) := fun _ _ h =>
  Exists.imp fun _ hs => ⟨hs.1, hf _ hs.1 h hs.2⟩

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