English
In Alexandrov-discrete spaces, the preimage of a set under the canonical map to the specialization is open iff the set is an upper set.
Русский
В пространствах Александрова-дискретности предобраз множества по каноническому отображению в специализацию является открытым тогда и только тогда, когда множество является верхним множеством.
LaTeX
$$$[AlexandrovDiscrete(\alpha)] \Rightarrow (IsOpen(toEquiv^{-1}(s)) \iff IsUpperSet(s))$$$
Lean4
/-- A recursor for `Specialization`. Use as `induction x`. -/
@[elab_as_elim, cases_eliminator, induction_eliminator]
protected def rec {β : Specialization α → Sort*} (h : ∀ a, β (toEquiv a)) (a : Specialization α) : β a :=
h (ofEquiv a)
