generateFrom_surjective — Mathlib

English

The map generateFrom: Set(Set α) → TopologicalSpace α is surjective; every topology on α is generated by its collection of open sets.

Русский

Отображение generateFrom: Set(Set α) → TopologicalSpace α сюрьективно; каждая топология на α порождается своим множеством открытых множеств.

LaTeX

$$Surjective( generateFrom : Set(Set α) → TopologicalSpace α )$$

Lean4

theorem generateFrom_surjective : Surjective (generateFrom : Set (Set α) → TopologicalSpace α) :=
  (gciGenerateFrom α).u_surjective

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