map_unique — Mathlib

English

If g is uniform continuous and ∀ a ∈ α, ↑(f a) = g a, then Completion.map f = g.

Русский

Если g непрерывно по униформности и ∀ a ∈ α, ↑(f a) = g a, то Completion.map f = g.

LaTeX

$$$\\mathrm{UniformContinuous}\, g \\to (\\forall a:\\alpha, \\uparrow( f(a)) = g(a)) \\to \\mathrm{Completion.map} f = g$$$

Lean4

theorem map_unique {f : α → β} {g : Completion α → Completion β} (hg : UniformContinuous g)
    (h : ∀ a : α, ↑(f a) = g a) : Completion.map f = g :=
  cPkg.map_unique cPkg hg h

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