Theorems · Theorem · general topology

AbstractCompletion.funext

∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ}
  [inst_1 : TopologicalSpace β] [T2Space β] {f g : pkg.space → β},
  Continuous f → Continuous g → (∀ (a : α), f (pkg.coe a) = g (pkg.coe a)) → f = g

Defined in

Mathlib.Topology.UniformSpace.AbstractCompletion

Cited by

5 results in Mathlib

Foundations

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

Assumes

UniformSpaceTopologicalSpaceT2Space