isOpen_preimage_ofLower — Mathlib

English

For every subset s of α, the preimage of s under the map ofLower is open in WithLower α if and only if s is open in the lower topology on α.

Русский

Для любой подмножества s ⊆ α предобразом через отображение ofLower является открытое множество в WithLower α тогда, когда s открыто в нижней топологии на α.

LaTeX

$$$\\forall s : Set \\; \\alpha,\\ IsOpen(\\operatorname{ofLower}^{-1} s) \\iff IsOpen[lower \\alpha]\, s$$$

Lean4

theorem isOpen_preimage_ofLower : IsOpen (ofLower ⁻¹' s) ↔ IsOpen[lower α] s :=
  Iff.rfl

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