isOpen_ofLowerSet_preimage — Mathlib

English

For a subset s of WithUpperSet α, IsOpen (toUpperSet ⁻¹' s) is equivalent to IsUpperSet s.

Русский

Для подмножества s пространства WithUpperSet α, IsOpen (toUpperSet⁻¹' s) эквивалентно IsUpperSet s.

LaTeX

$$$IsOpen(\\mathrm{toUpperSet}^{-1}(s)) \\iff IsUpperSet(s).$$$

Lean4

@[simp]
theorem isOpen_ofLowerSet_preimage {s : Set α} : IsOpen (ofLowerSet ⁻¹' s) ↔ IsLowerSet s :=
  isLowerSet_toLowerSet_preimage.symm

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