stableUnderSpecialization_iUnion — Mathlib

English

If each S(i) is stable under specialization, then the union across i is stable under specialization.

Русский

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

LaTeX

$$$\forall i, StableUnderSpecialization(S(i)) \Rightarrow StableUnderSpecialization\left(\bigcup_i S(i)\right)$$$

Lean4

theorem stableUnderSpecialization_iUnion {ι : Sort*} (S : ι → Set X) (H : ∀ i, StableUnderSpecialization (S i)) :
    StableUnderSpecialization (⋃ i, S i) :=
  isLowerSet_iUnion H

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