Theorems · Theorem · general topology

AbstractCompletion.compare_comp_eq_compare

∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) (pkg' : AbstractCompletion.{vα', uα} α)
  (γ : Type uγ) [inst_1 : TopologicalSpace γ] [T3Space γ] {f : α → γ},
  Continuous f →
    (∀ (a : pkg.space), Filter.Tendsto f (Filter.comap pkg.coe (nhds a)) (nhds (⋯.extend f a))) →
      ⋯.extend f ∘ pkg'.compare pkg = ⋯.extend f

Defined in

Mathlib.Topology.UniformSpace.AbstractCompletion

Cited by

1 results in Mathlib

Foundations

Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

UniformSpaceTopologicalSpaceT3Space