Theorems · Definition · general topology

UniformEquiv.subtype

{α : Type u} →
  {β : Type u_1} →
    [inst : UniformSpace α] →
      [inst_1 : UniformSpace β] →
        {p : α → Prop} → {q : β → Prop} → (e : α ≃ᵤ β) → (∀ (a : α), p a ↔ q (e a)) → { a // p a } ≃ᵤ { b // q b }

A uniform isomorphism e : α ≃ᵤ β lifts to subtypes { a : α // p a } ≃ᵤ { b : β // q b } provided p = q ∘ e.

Defined in

Mathlib.Topology.UniformSpace.Equiv

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpaceUniformSpace