isUpperSet_toUpperSet_preimage — Mathlib

English

For any subset s of WithUpperSet α, the preimage under the canonical embedding is upper-set iff s is open, i.e., IsUpperSet (toUpperSet⁻¹' s) ↔ IsOpen s.

Русский

Для любой подмножества s пространства WithUpperSet α, его предобраз при каноническом вложении является верхним множеством тогда и только тогда, когда s открыто. То есть IsUpperSet(toUpperSet⁻¹' s) ↔ IsOpen s.

LaTeX

$$$\\forall s \\subseteq \\mathrm{WithUpperSet}(\\alpha),\\; \\mathrm{IsUpperSet}(\\mathrm{toUpperSet}^{-1}(s)) \\iff \\mathrm{IsOpen}(s).$$$

Lean4

@[simp]
theorem isUpperSet_toUpperSet_preimage {s : Set (WithUpperSet α)} : IsUpperSet (toUpperSet ⁻¹' s) ↔ IsOpen s :=
  Iff.rfl

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