English
A refined version of the previous extension result under a chosen condition; there exists an extension limit that satisfies a family of equations.
Русский
Уточнённая версия результата продолжения с заданным условием; существует предел продолжения, удовлетворяющий целому набору условий.
LaTeX
$$$\text{Under the matched conditioning, there exists } c \text{ with Tendsto } \!f\! (\,! ) (\nhds c).$$$
Lean4
theorem uniform_extend_subtype [CompleteSpace γ] {p : α → Prop} {e : α → β} {f : α → γ} {b : β} {s : Set α}
(hf : UniformContinuous fun x : Subtype p => f x.val) (he : IsUniformEmbedding e)
(hd : ∀ x : β, x ∈ closure (range e)) (hb : closure (e '' s) ∈ 𝓝 b) (hs : IsClosed s) (hp : ∀ x ∈ s, p x) :
∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c) :=
by
have de : IsDenseEmbedding e := he.isDenseEmbedding hd
have de' : IsDenseEmbedding (IsDenseEmbedding.subtypeEmb p e) := de.subtype p
have ue' : IsUniformEmbedding (IsDenseEmbedding.subtypeEmb p e) := isUniformEmbedding_subtypeEmb _ he de
have : b ∈ closure (e '' {x | p x}) := (closure_mono <| monotone_image <| hp) (mem_of_mem_nhds hb)
let ⟨c, hc⟩ := uniformly_extend_exists ue'.isUniformInducing de'.dense hf ⟨b, this⟩
replace hc : Tendsto (f ∘ Subtype.val (p := p)) (((𝓝 b).comap e).comap Subtype.val) (𝓝 c) := by
simpa only [nhds_subtype_eq_comap, comap_comap, IsDenseEmbedding.subtypeEmb_coe] using hc
refine ⟨c, (tendsto_comap'_iff ?_).1 hc⟩
rw [Subtype.range_coe_subtype]
exact ⟨_, hb, by rwa [← de.isInducing.closure_eq_preimage_closure_image, hs.closure_eq]⟩
