stableUnderGeneralization_sInter — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem stableUnderGeneralization_sInter (S : Set (Set X)) (H : ∀ s ∈ S, StableUnderGeneralization s) :
    StableUnderGeneralization (⋂₀ S) :=
  isUpperSet_sInter H

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