isUpperSet_ofEquiv_preimage — Mathlib

English

An upper set preimage characterization: IsUpperSet (toEquiv^{-1}' s) iff IsOpen s.

Русский

Характеризация верхних множеств через прообраз: IsUpperSet (toEquiv^{-1}' s) эквивалентно IsOpen s.

LaTeX

$$$[AlexandrovDiscrete(\alpha)]\; {s:\text{Set}(\alpha)}:\; IsUpperSet(toEquiv^{-1}(s)) \iff IsOpen(s)$$$

Lean4

@[simp]
theorem isUpperSet_ofEquiv_preimage [AlexandrovDiscrete α] {s : Set α} : IsUpperSet (ofEquiv ⁻¹' s) ↔ IsOpen s :=
  isOpen_toEquiv_preimage.symm

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