mkOfClosure_sets — Mathlib

English

If hs states that the open sets of the generated topology coincide with s, then mkOfClosure s hs equals generateFrom s; i.e., the two constructions yield the same topology.

Русский

Если hs говорит, что открытые множества порождаемой топологии совпадают с s, то mkOfClosure s hs равно generateFrom s; то есть оба построения дают одну и ту же топологию.

LaTeX

$$$\\mathrm{mkOfClosure}\\;s\\;hs = \\mathrm{generateFrom}\\;s$$$

Lean4

theorem mkOfClosure_sets {s : Set (Set α)} {hs : {u | GenerateOpen s u} = s} :
    TopologicalSpace.mkOfClosure s hs = generateFrom s :=
  TopologicalSpace.ext hs.symm

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