leftInverse_generateFrom — Mathlib

English

There is a left inverse relationship between the operation that takes a topology to its open-sets and the operation that generates a topology from a collection of sets.

Русский

Существует левая обратная зависимость между отображением топологии в множество открытых множеств и отображением, порождающим топологию из множества подмножеств.

LaTeX

$$LeftInverse( generateFrom, (\\lambda t. {s \\mid IsOpen[t] s}))$$

Lean4

theorem leftInverse_generateFrom : LeftInverse generateFrom fun t : TopologicalSpace α => {s | IsOpen[t] s} :=
  (gciGenerateFrom α).u_l_leftInverse

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