specializes_iff_forall_closed — Mathlib

English

x specializes to y if and only if for every open set s with y ∈ s, x ∈ s.

Русский

x специализируется на y тогда и только тогда, когда для каждого открытого множества s, если y ∈ s, то x ∈ s.

LaTeX

$$$ x ⤳ y \iff \forall s, IsOpen(s) \to y \in s \to x \in s$$$

Lean4

theorem specializes_iff_forall_closed : x ⤳ y ↔ ∀ s : Set X, IsClosed s → x ∈ s → y ∈ s :=
  (specializes_TFAE x y).out 0 3

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