topology_eq — Mathlib

English

If IsScottHausdorff α D holds, then the given topology on α coincides with the Scott-Hausdorff topology, i.e. τ = scottHausdorff α D.

Русский

Если выполняется свойство IsScottHausdorff для α и D, то данная топология на α совпадает с топологией Scott-Hausdorff, т.е. τ = scottHausdorff α D.

LaTeX

$$$\\tau = \\mathrm{scottHausdorff}(\\alpha, D)$$$

Lean4

theorem topology_eq [IsScottHausdorff α D] : ‹_› = scottHausdorff α D :=
  topology_eq_scottHausdorff

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