stableUnderGeneralization_sUnion — Mathlib

English

If each s in a family S of sets is stable under generalization, then their union is stable under generalization.

Русский

Если каждый элемент семейства S подмножеств устойчив по обобщению, то их объединение устойчиво по обобщению.

LaTeX

$$$\Big(\forall s\in S, StableUnderGeneralization(s)\Big) \Rightarrow StableUnderGeneralization(\bigcup_{s\in S} s)$$$

Lean4

theorem stableUnderGeneralization_sUnion (S : Set (Set X)) (H : ∀ s ∈ S, StableUnderGeneralization s) :
    StableUnderGeneralization (⋃₀ S) :=
  isUpperSet_sUnion H

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