Theorems · Theorem · general topology

UniformOnFun.uniformSpace_eq_inf_precomp_of_cover

∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] (𝔖 : Set (Set α)) {δ₁ : Type u_5} {δ₂ : Type u_6} (φ₁ : δ₁ → α)
  (φ₂ : δ₂ → α) (𝔗₁ : Set (Set δ₁)) (𝔗₂ : Set (Set δ₂)),
  Set.MapsTo (fun x => φ₁ '' x) 𝔗₁ 𝔖 →
    Set.MapsTo (fun x => φ₂ '' x) 𝔗₂ 𝔖 →
      Set.MapsTo (fun x => φ₁ ⁻¹' x) 𝔖 𝔗₁ →
        Set.MapsTo (fun x => φ₂ ⁻¹' x) 𝔖 𝔗₂ →
          (∀ S ∈ 𝔖, S ⊆ Set.range φ₁ ∪ Set.range φ₂) →
            UniformOnFun.uniformSpace α β 𝔖 =
              UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔗₁) ∘ (fun x => x ∘ φ₁) ∘ ⇑(UniformOnFun.toFun 𝔖))
                  (UniformOnFun.uniformSpace δ₁ β 𝔗₁) ⊓
                UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔗₂) ∘ (fun x => x ∘ φ₂) ∘ ⇑(UniformOnFun.toFun 𝔖))
                  (UniformOnFun.uniformSpace δ₂ β 𝔗₂)

Defined in

Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Cited by

1 results in Mathlib

Foundations

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

Assumes

UniformSpace