English
Construct a UniformSpace from UniformSpace.Core and a TopologicalSpace equal to its toTopologicalSpace.
Русский
Построить UniformSpace из UniformSpace.Core и топологической структуры, равной его toTopologicalSpace.
LaTeX
$$$\\text{ofCoreEq }(u: UniformSpace.Core\\,\\alpha)\\; (t: TopologicalSpace\\alpha)\\; (h: t = u.toCore.toTopologicalSpace) : UniformSpace\\alpha$$$
Lean4
/-- Construct a `UniformSpace` from a `u : UniformSpace.Core` and a `TopologicalSpace` structure
that is equal to `u.toTopologicalSpace`. -/
abbrev ofCoreEq {α : Type u} (u : UniformSpace.Core α) (t : TopologicalSpace α) (h : t = u.toTopologicalSpace) :
UniformSpace α where
__ := u
toTopologicalSpace := t
nhds_eq_comap_uniformity x := by rw [h, u.nhds_toTopologicalSpace]
