stableUnderSpecialization_sInter — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem stableUnderSpecialization_sInter (S : Set (Set X)) (H : ∀ s ∈ S, StableUnderSpecialization s) :
    StableUnderSpecialization (⋂₀ S) :=
  isLowerSet_sInter H

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