English
In Alexandrov-discrete spaces, the preimage under toEquiv is open iff the subset is an upper set.
Русский
В пространствах Александрова-дискретных предобраз под toEquiv открыт тогда и только тогда, когда подмножество является верхним множеством.
LaTeX
$$$[AlexandrovDiscrete(\alpha)]\; {s\subseteq (Specialization(\alpha))}:\; IsOpen(toEquiv^{-1}(s)) \iff IsUpperSet(s)$$$
Lean4
@[simp]
theorem isOpen_toEquiv_preimage [AlexandrovDiscrete α] {s : Set (Specialization α)} :
IsOpen (toEquiv ⁻¹' s) ↔ IsUpperSet s :=
isOpen_iff_forall_specializes.trans forall_swap