isOpen_iff — Mathlib

English

A subset U of PT L is open iff there exists u ∈ L with U = {x | x u}.

Русский

Подмножество U пространства PT L открыто тогда и только тогда, когда существует элемент u ∈ L и U = \{x | x u\}.

LaTeX

$$IsOpen(U) $\iff$ ∃ u: L, {x | x u} = U$$

Lean4

/-- Characterization of when a subset of the space of points is open. -/
theorem isOpen_iff (U : Set (PT L)) : IsOpen U ↔ ∃ u : L, {x | x u} = U :=
  Iff.rfl

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