Theorems · Theorem · general topology

uniform_extend_subtype

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace α] [inst_1 : UniformSpace β]
  [inst_2 : UniformSpace γ] [CompleteSpace γ] {p : α → Prop} {e : α → β} {f : α → γ} {b : β} {s : Set α},
  (UniformContinuous fun x => f ↑x) →
    IsUniformEmbedding e →
      (∀ (x : β), x ∈ closure (Set.range e)) →
        closure (e '' s) ∈ nhds b →
          IsClosed s → (∀ x ∈ s, p x) → ∃ c, Filter.Tendsto f (Filter.comap e (nhds b)) (nhds c)

Defined in

Mathlib.Topology.UniformSpace.UniformEmbedding

Cited by

0 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

UniformSpaceUniformSpaceUniformSpaceCompleteSpace