isOpen_def — Mathlib

English

For any subset T of WithLower α, T is open in the WithLower topology if and only if the preimage under toLower is open in the lower topology on α.

Русский

Для любой подмножества T ∈ Set(WithLower α) множество T открыто в нижней топологии тогда, когда предварительный образ T под действием toLower открыт в нижней топологии на α.

LaTeX

$$$\\forall T : Set(WithLower \\alpha),\\ IsOpen T \\iff IsOpen[lower \\alpha] (toLower^{-1} T)$$$

Lean4

theorem isOpen_def (T : Set (WithLower α)) : IsOpen T ↔ IsOpen[lower α] (WithLower.toLower ⁻¹' T) :=
  Iff.rfl

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