stableUnderSpecialization_sUnion — Mathlib

English

If each member of a family S of subsets is stable under specialization, then their union is stable under specialization.

Русский

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

LaTeX

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

Lean4

theorem stableUnderSpecialization_sUnion (S : Set (Set X)) (H : ∀ s ∈ S, StableUnderSpecialization s) :
    StableUnderSpecialization (⋃₀ S) :=
  isLowerSet_sUnion H

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