mk' — Mathlib

English

In a T3-space, if the tail condition hf holds for all b, then di.extend f is continuous.

Русский

Для каждого b условие hf даёт непрерывность di.extend f.

LaTeX

$$$[T3Space γ] \\\\forall b, \\\\exists c, Tendsto f (comap i (\\\\mathcal{N} b)) (\\\\mathcal{N} c) \\\\Rightarrow \\\\text{ContinuousAt}(\\\\mathrm{extend} f) b$$$

Lean4

theorem mk' [TopologicalSpace α] [TopologicalSpace β] (e : α → β) (c : Continuous e) (dense : DenseRange e)
    (injective : Function.Injective e) (H : ∀ (a : α), ∀ s ∈ 𝓝 a, ∃ t ∈ 𝓝 (e a), ∀ b, e b ∈ t → b ∈ s) :
    IsDenseEmbedding e :=
  { IsDenseInducing.mk' e c dense H with injective }

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