stableUnderGeneralization_iUnion — Mathlib

English

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

Русский

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

LaTeX

$$$\forall i, StableUnderGeneralization(S(i)) \Rightarrow StableUnderGeneralization(\bigcup_i S(i))$$$

Lean4

theorem stableUnderGeneralization_iUnion {ι : Sort*} (S : ι → Set X) (H : ∀ i, StableUnderGeneralization (S i)) :
    StableUnderGeneralization (⋃ i, S i) :=
  isUpperSet_iUnion H

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