not_specializes_iff_exists_closed

English

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

Русский

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

LaTeX

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

Lean4

theorem not_specializes_iff_exists_closed : ¬x ⤳ y ↔ ∃ S : Set X, IsClosed S ∧ x ∈ S ∧ y ∉ S :=
  by
  rw [specializes_iff_forall_closed]
  push_neg
  rfl

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