IsOpen — Mathlib

English

A set is open in a topological space if it is an element of the topology on that space.

Русский

Множество открыто в топологическом пространстве, если оно принадлежит топологии над этим пространством.

LaTeX

$$$\text{IsOpen}(s) := \text{TopologicalSpace.IsOpen}(s)$$$

Lean4

/-- `IsOpen s` means that `s` is open in the ambient topological space on `X` -/
def IsOpen : Set X → Prop :=
  TopologicalSpace.IsOpen

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