injective_restrict — Mathlib

English

If s is dense in a T2 space β, then the restriction map from C(α,β) to C(s,β) is injective.

Русский

Если s плотно в T2-пространстве β, то отображение ограничения из C(α,β) в C(s,β) инъективно.

LaTeX

$$$[T2Space\;\beta]\; {s: Set\;\alpha} \Rightarrow \mathrm{Injective}(\mathrm{restrict}\;s)$$$

Lean4

theorem injective_restrict [T2Space β] {s : Set α} (hs : Dense s) : Injective (restrict s : C(α, β) → C(s, β)) :=
  fun f g h ↦
  DFunLike.ext' <|
    (map_continuous f).ext_on hs (map_continuous g) <| Set.restrict_eq_restrict_iff.1 <| congr_arg DFunLike.coe h

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