map_unique — Mathlib

English

If two uniform continuous maps agree on the dense image of α, then they coincide as maps on hatα.

Русский

Если два равномерно непрерывных отображения совпадают на образе α, тогда они совпадают на hatα.

LaTeX

$$$ (hg: UniformContinuous g) \\to (\forall a, ι' (f a) = g (ι a)) \\to Eq (pkg.map pkg' f) g $$$

Lean4

theorem map_unique {f : α → β} {g : hatα → hatβ} (hg : UniformContinuous g) (h : ∀ a, ι' (f a) = g (ι a)) : map f = g :=
  pkg.funext (pkg.continuous_map _ _) hg.continuous <| by
    intro a
    change pkg.extend (ι' ∘ f) _ = _
    simp_rw [Function.comp_def, h, ← comp_apply (f := g)]
    rw [pkg.extend_coe (hg.comp pkg.uniformContinuous_coe)]

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