isLowerSet_sUnion — Mathlib

English

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

Русский

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

LaTeX

$$$\forall S. (S \subseteq \mathcal{P}(\alpha) \text{ и } \forall s ∈ S, IsLowerSet(s)) \Rightarrow IsLowerSet(\bigcup S)$$$

Lean4

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

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