StableUnderGeneralization — Mathlib

English

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

Русский

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

LaTeX

$$$$ StableUnderGeneralization(S) := \forall \{x,y\},\ y \rightsquigarrow x \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 `y ⤳ x`. -/
def StableUnderGeneralization (s : Set X) : Prop :=
  ∀ ⦃x y⦄, y ⤳ x → x ∈ s → y ∈ s

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