inseparable_extend — Mathlib

English

If γ is an R1 space, then the extended value is inseparable from f(a).

Русский

Если γ — пространство R1, то продолженная величина неразделимо близка к f(a).

LaTeX

$$$\\text{inseparable_extend }(di)(f)(a) : \\text{Inseparable}(di.extend f (i a), f a)$$$

Lean4

theorem inseparable_extend [R1Space γ] (di : IsDenseInducing i) {f : α → γ} {a : α} (hf : ContinuousAt f a) :
    Inseparable (di.extend f (i a)) (f a) :=
  tendsto_nhds_unique_inseparable (di.tendsto_extend hf) hf

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