toTopsp — Mathlib

English

Every Ctop yields a topological space by generating the topology from its open sets.

Русский

Каждый Ctop определяет топологическое пространство, порождаемое открытыми множествами.

LaTeX

$$$\\text{toTopsp}(F) = \\text{TopologicalSpace}(\\text{range } F.f)$$$

Lean4

/-- Every `Ctop` is a topological space. -/
def toTopsp (F : Ctop α σ) : TopologicalSpace α :=
  TopologicalSpace.generateFrom (Set.range F.f)

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