isOpen_def — Mathlib

English

A set is open in WithLawson α iff its preimage under the toLawson map is open in the Lawson topology on α.

Русский

Множество открыто в WithLawson α тогда и только тогда, когда его образ обратного образа через toLawson открыто в Lawson topology на α.

LaTeX

$$$IsOpen(T) \iff (lawson(\alpha)).IsOpen (toLawson^{-1}(T))$$$

Lean4

theorem isOpen_def {T : Set (WithLawson α)} : IsOpen T ↔ (lawson α).IsOpen (toLawson ⁻¹' T) :=
  Iff.rfl

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