isOpen_toEquiv_preimage — Mathlib

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

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