StableUnderSpecialization — Mathlib

English

A subset S is stable under specialization if whenever x ⤳ y and x ∈ S, then y ∈ S.

Русский

Подмножество S стабильно по отношению к специализации, если при x ⤳ y и x ∈ S следует y ∈ S.

LaTeX

$$$$ StableUnderSpecialization(S) := \forall \{x,y\},\ x \rightsquigarrow y \rightarrow x \in S \rightarrow y \in S. $$$$

Lean4

/-- A subset `S` of a topological space is stable under specialization
if `x ∈ S → y ∈ S` for all `x ⤳ y`. -/
def StableUnderSpecialization (s : Set X) : Prop :=
  ∀ ⦃x y⦄, x ⤳ y → x ∈ s → y ∈ s

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