specializes_iff_forall_open — Mathlib

English

x specializes to y if and only if for every open set s, y ∈ s implies 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_open : x ⤳ y ↔ ∀ s : Set X, IsOpen s → y ∈ s → x ∈ s :=
  (specializes_TFAE x y).out 0 2

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