not_specializes_iff_exists_open — Mathlib

English

There exists an open set separating x and y in the sense of not specializing: not x ⤳ y iff there exists an open set containing y but not x.

Русский

Существуют открытые множества, отделяющие x и y по отношению к не-специализации: не x ⤳ y эквивалентно существованию открытого множества, содержащего y, но не x.

LaTeX

$$$$ \neg(x \rightsquigarrow y) \iff \exists S, IsOpen S \land y \in S \land x \notin S. $$$$

Lean4

theorem not_specializes_iff_exists_open : ¬x ⤳ y ↔ ∃ S : Set X, IsOpen S ∧ y ∈ S ∧ x ∉ S :=
  by
  rw [specializes_iff_forall_open]
  push_neg
  rfl

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