[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
⊢ GaloisConnection (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α β 𝓕
[PROOFSTEP]
intro 𝓐 𝓕
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) 𝓐 ≤ 𝓕 ↔ 𝓐 ≤ (fun 𝓕 => UniformFun.filter α β 𝓕) 𝓕
[PROOFSTEP]
symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ 𝓐 ≤ (fun 𝓕 => UniformFun.filter α β 𝓕) 𝓕 ↔ (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) 𝓐 ≤ 𝓕
[PROOFSTEP]
calc
  𝓐 ≤ UniformFun.filter α β 𝓕 ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets := by
    rw [UniformFun.filter, ← FilterBasis.generate, le_generate_iff]
  _ ↔ ∀ U ∈ 𝓕, UniformFun.gen α β U ∈ 𝓐 := image_subset_iff
  _ ↔ ∀ U ∈ 𝓕, {uv | ∀ x, (uv, x) ∈ {t : ((α →ᵤ β) × (α →ᵤ β)) × α | (t.1.1 t.2, t.1.2 t.2) ∈ U}} ∈ 𝓐 := Iff.rfl
  _ ↔ ∀ U ∈ 𝓕, {uvx : ((α →ᵤ β) × (α →ᵤ β)) × α | (uvx.1.1 uvx.2, uvx.1.2 uvx.2) ∈ U} ∈ 𝓐 ×ˢ (⊤ : Filter α) :=
    (forall₂_congr fun U _hU => mem_prod_top.symm)
  _ ↔ lower_adjoint 𝓐 ≤ 𝓕 := Iff.rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
𝓐 : Filter ((α →ᵤ β) × (α →ᵤ β))
𝓕 : Filter (β × β)
⊢ 𝓐 ≤ UniformFun.filter α β 𝓕 ↔ (UniformFun.basis α β 𝓕).sets ⊆ 𝓐.sets
[PROOFSTEP]
rw [UniformFun.filter, ← FilterBasis.generate, le_generate_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x✝ : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
x : α
⊢ UniformContinuous (Function.eval x ∘ ↑toFun)
[PROOFSTEP]
change _ ≤ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x✝ : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
x : α
⊢ map (fun x_1 => ((Function.eval x ∘ ↑toFun) x_1.fst, (Function.eval x ∘ ↑toFun) x_1.snd)) (𝓤 (α →ᵤ β)) ≤ 𝓤 β
[PROOFSTEP]
rw [map_le_iff_le_comap, (UniformFun.hasBasis_uniformity α β).le_basis_iff ((𝓤 _).basis_sets.comap _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x✝ : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
x : α
⊢ ∀ (i' : Set (β × β)),
    i' ∈ 𝓤 β →
      ∃ i,
        i ∈ 𝓤 β ∧
          UniformFun.gen α β i ⊆
            (fun x_1 => ((Function.eval x ∘ ↑toFun) x_1.fst, (Function.eval x ∘ ↑toFun) x_1.snd)) ⁻¹' id i'
[PROOFSTEP]
exact fun U hU => ⟨U, hU, fun uv huv => huv x⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
u : ι → UniformSpace γ
⊢ uniformSpace α γ = ⨅ (i : ι), uniformSpace α γ
[PROOFSTEP]
ext : 1
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
u : ι → UniformSpace γ
⊢ 𝓤 (α →ᵤ γ) = 𝓤 (α →ᵤ γ)
[PROOFSTEP]
change UniformFun.filter α γ 𝓤[⨅ i, u i] = 𝓤[⨅ i, 𝒰(α, γ, u i)]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
u : ι → UniformSpace γ
⊢ UniformFun.filter α γ (𝓤 γ) = 𝓤 (α →ᵤ γ)
[PROOFSTEP]
rw [iInf_uniformity, iInf_uniformity]
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
u : ι → UniformSpace γ
⊢ UniformFun.filter α γ (⨅ (i : ι), 𝓤 γ) = ⨅ (i : ι), 𝓤 (α →ᵤ γ)
[PROOFSTEP]
exact (UniformFun.gc α γ).u_iInf
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
u₁ u₂ : UniformSpace γ
⊢ uniformSpace α γ = uniformSpace α γ ⊓ uniformSpace α γ
[PROOFSTEP]
rw [inf_eq_iInf, inf_eq_iInf, UniformFun.iInf_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
u₁ u₂ : UniformSpace γ
⊢ ⨅ (i : Bool), uniformSpace α γ = ⨅ (b : Bool), bif b then uniformSpace α γ else uniformSpace α γ
[PROOFSTEP]
refine' iInf_congr fun i => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
u₁ u₂ : UniformSpace γ
i : Bool
⊢ uniformSpace α γ = bif i then uniformSpace α γ else uniformSpace α γ
[PROOFSTEP]
cases i
[GOAL]
case false
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
u₁ u₂ : UniformSpace γ
⊢ uniformSpace α γ = bif false then uniformSpace α γ else uniformSpace α γ
[PROOFSTEP]
rfl
[GOAL]
case true
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
u₁ u₂ : UniformSpace γ
⊢ uniformSpace α γ = bif true then uniformSpace α γ else uniformSpace α γ
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → β
⊢ uniformSpace α γ = UniformSpace.comap (fun x => f ∘ x) (uniformSpace α β)
[PROOFSTEP]
letI : UniformSpace γ := ‹UniformSpace β›.comap f
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → β
this : UniformSpace γ := UniformSpace.comap f inst✝
⊢ uniformSpace α γ = UniformSpace.comap (fun x => f ∘ x) (uniformSpace α β)
[PROOFSTEP]
ext : 1
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → β
this : UniformSpace γ := UniformSpace.comap f inst✝
⊢ 𝓤 (α →ᵤ γ) = 𝓤 (α →ᵤ γ)
[PROOFSTEP]
change
  UniformFun.filter α γ ((𝓤 β).comap _) =
    (UniformFun.filter α β (𝓤 β)).comap
      _
        -- We have the following four Galois connection which form a square diagram, and we want
          -- to show that the square of upper adjoints is commutative. The trick then is to use
          -- `GaloisConnection.u_comm_of_l_comm` to reduce it to commutativity of the lower adjoints,
          -- which is way easier to prove.
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → β
this : UniformSpace γ := UniformSpace.comap f inst✝
⊢ UniformFun.filter α γ (comap (fun p => (f p.fst, f p.snd)) (𝓤 β)) =
    comap (fun p => ((fun x => f ∘ x) p.fst, (fun x => f ∘ x) p.snd)) (UniformFun.filter α β (𝓤 β))
[PROOFSTEP]
let fcomp := ((f ∘ ·) : ((α → γ) → (α → β)))
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → β
this : UniformSpace γ := UniformSpace.comap f inst✝
fcomp : (α → γ) → α → β := fun x => f ∘ x
⊢ UniformFun.filter α γ (comap (fun p => (f p.fst, f p.snd)) (𝓤 β)) =
    comap (fun p => ((fun x => f ∘ x) p.fst, (fun x => f ∘ x) p.snd)) (UniformFun.filter α β (𝓤 β))
[PROOFSTEP]
have h₁ := Filter.gc_map_comap (Prod.map fcomp fcomp)
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → β
this : UniformSpace γ := UniformSpace.comap f inst✝
fcomp : (α → γ) → α → β := fun x => f ∘ x
h₁ : GaloisConnection (map (Prod.map fcomp fcomp)) (comap (Prod.map fcomp fcomp))
⊢ UniformFun.filter α γ (comap (fun p => (f p.fst, f p.snd)) (𝓤 β)) =
    comap (fun p => ((fun x => f ∘ x) p.fst, (fun x => f ∘ x) p.snd)) (UniformFun.filter α β (𝓤 β))
[PROOFSTEP]
have h₂ := Filter.gc_map_comap (Prod.map f f)
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → β
this : UniformSpace γ := UniformSpace.comap f inst✝
fcomp : (α → γ) → α → β := fun x => f ∘ x
h₁ : GaloisConnection (map (Prod.map fcomp fcomp)) (comap (Prod.map fcomp fcomp))
h₂ : GaloisConnection (map (Prod.map f f)) (comap (Prod.map f f))
⊢ UniformFun.filter α γ (comap (fun p => (f p.fst, f p.snd)) (𝓤 β)) =
    comap (fun p => ((fun x => f ∘ x) p.fst, (fun x => f ∘ x) p.snd)) (UniformFun.filter α β (𝓤 β))
[PROOFSTEP]
have h₃ := UniformFun.gc α β
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → β
this : UniformSpace γ := UniformSpace.comap f inst✝
fcomp : (α → γ) → α → β := fun x => f ∘ x
h₁ : GaloisConnection (map (Prod.map fcomp fcomp)) (comap (Prod.map fcomp fcomp))
h₂ : GaloisConnection (map (Prod.map f f)) (comap (Prod.map f f))
h₃ : GaloisConnection (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α β 𝓕
⊢ UniformFun.filter α γ (comap (fun p => (f p.fst, f p.snd)) (𝓤 β)) =
    comap (fun p => ((fun x => f ∘ x) p.fst, (fun x => f ∘ x) p.snd)) (UniformFun.filter α β (𝓤 β))
[PROOFSTEP]
have h₄ := UniformFun.gc α γ
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → β
this : UniformSpace γ := UniformSpace.comap f inst✝
fcomp : (α → γ) → α → β := fun x => f ∘ x
h₁ : GaloisConnection (map (Prod.map fcomp fcomp)) (comap (Prod.map fcomp fcomp))
h₂ : GaloisConnection (map (Prod.map f f)) (comap (Prod.map f f))
h₃ : GaloisConnection (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α β 𝓕
h₄ : GaloisConnection (fun 𝓐 => map (UniformFun.phi α γ) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α γ 𝓕
⊢ UniformFun.filter α γ (comap (fun p => (f p.fst, f p.snd)) (𝓤 β)) =
    comap (fun p => ((fun x => f ∘ x) p.fst, (fun x => f ∘ x) p.snd)) (UniformFun.filter α β (𝓤 β))
[PROOFSTEP]
refine' GaloisConnection.u_comm_of_l_comm h₁ h₂ h₃ h₄ fun 𝓐 => _
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → β
this : UniformSpace γ := UniformSpace.comap f inst✝
fcomp : (α → γ) → α → β := fun x => f ∘ x
h₁ : GaloisConnection (map (Prod.map fcomp fcomp)) (comap (Prod.map fcomp fcomp))
h₂ : GaloisConnection (map (Prod.map f f)) (comap (Prod.map f f))
h₃ : GaloisConnection (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α β 𝓕
h₄ : GaloisConnection (fun 𝓐 => map (UniformFun.phi α γ) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α γ 𝓕
𝓐 : Filter ((α → γ) × (α → γ))
⊢ map (Prod.map f f) (map (UniformFun.phi α γ) (𝓐 ×ˢ ⊤)) = map (UniformFun.phi α β) (map (Prod.map fcomp fcomp) 𝓐 ×ˢ ⊤)
[PROOFSTEP]
have : Prod.map f f ∘ (UniformFun.phi α γ) = (UniformFun.phi α β) ∘ Prod.map (Prod.map fcomp fcomp) (id : α → α) := by
  ext <;> rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → β
this : UniformSpace γ := UniformSpace.comap f inst✝
fcomp : (α → γ) → α → β := fun x => f ∘ x
h₁ : GaloisConnection (map (Prod.map fcomp fcomp)) (comap (Prod.map fcomp fcomp))
h₂ : GaloisConnection (map (Prod.map f f)) (comap (Prod.map f f))
h₃ : GaloisConnection (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α β 𝓕
h₄ : GaloisConnection (fun 𝓐 => map (UniformFun.phi α γ) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α γ 𝓕
𝓐 : Filter ((α → γ) × (α → γ))
⊢ Prod.map f f ∘ UniformFun.phi α γ = UniformFun.phi α β ∘ Prod.map (Prod.map fcomp fcomp) id
[PROOFSTEP]
ext
[GOAL]
case h.h₁
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → β
this : UniformSpace γ := UniformSpace.comap f inst✝
fcomp : (α → γ) → α → β := fun x => f ∘ x
h₁ : GaloisConnection (map (Prod.map fcomp fcomp)) (comap (Prod.map fcomp fcomp))
h₂ : GaloisConnection (map (Prod.map f f)) (comap (Prod.map f f))
h₃ : GaloisConnection (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α β 𝓕
h₄ : GaloisConnection (fun 𝓐 => map (UniformFun.phi α γ) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α γ 𝓕
𝓐 : Filter ((α → γ) × (α → γ))
x✝ : ((α →ᵤ γ) × (α →ᵤ γ)) × α
⊢ ((Prod.map f f ∘ UniformFun.phi α γ) x✝).fst = ((UniformFun.phi α β ∘ Prod.map (Prod.map fcomp fcomp) id) x✝).fst
[PROOFSTEP]
rfl
[GOAL]
case h.h₂
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → β
this : UniformSpace γ := UniformSpace.comap f inst✝
fcomp : (α → γ) → α → β := fun x => f ∘ x
h₁ : GaloisConnection (map (Prod.map fcomp fcomp)) (comap (Prod.map fcomp fcomp))
h₂ : GaloisConnection (map (Prod.map f f)) (comap (Prod.map f f))
h₃ : GaloisConnection (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α β 𝓕
h₄ : GaloisConnection (fun 𝓐 => map (UniformFun.phi α γ) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α γ 𝓕
𝓐 : Filter ((α → γ) × (α → γ))
x✝ : ((α →ᵤ γ) × (α →ᵤ γ)) × α
⊢ ((Prod.map f f ∘ UniformFun.phi α γ) x✝).snd = ((UniformFun.phi α β ∘ Prod.map (Prod.map fcomp fcomp) id) x✝).snd
[PROOFSTEP]
rfl
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → β
this✝ : UniformSpace γ := UniformSpace.comap f inst✝
fcomp : (α → γ) → α → β := fun x => f ∘ x
h₁ : GaloisConnection (map (Prod.map fcomp fcomp)) (comap (Prod.map fcomp fcomp))
h₂ : GaloisConnection (map (Prod.map f f)) (comap (Prod.map f f))
h₃ : GaloisConnection (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α β 𝓕
h₄ : GaloisConnection (fun 𝓐 => map (UniformFun.phi α γ) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α γ 𝓕
𝓐 : Filter ((α → γ) × (α → γ))
this : Prod.map f f ∘ UniformFun.phi α γ = UniformFun.phi α β ∘ Prod.map (Prod.map fcomp fcomp) id
⊢ map (Prod.map f f) (map (UniformFun.phi α γ) (𝓐 ×ˢ ⊤)) = map (UniformFun.phi α β) (map (Prod.map fcomp fcomp) 𝓐 ×ˢ ⊤)
[PROOFSTEP]
rw [map_comm this, ← prod_map_map_eq']
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → β
this✝ : UniformSpace γ := UniformSpace.comap f inst✝
fcomp : (α → γ) → α → β := fun x => f ∘ x
h₁ : GaloisConnection (map (Prod.map fcomp fcomp)) (comap (Prod.map fcomp fcomp))
h₂ : GaloisConnection (map (Prod.map f f)) (comap (Prod.map f f))
h₃ : GaloisConnection (fun 𝓐 => map (UniformFun.phi α β) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α β 𝓕
h₄ : GaloisConnection (fun 𝓐 => map (UniformFun.phi α γ) (𝓐 ×ˢ ⊤)) fun 𝓕 => UniformFun.filter α γ 𝓕
𝓐 : Filter ((α → γ) × (α → γ))
this : Prod.map f f ∘ UniformFun.phi α γ = UniformFun.phi α β ∘ Prod.map (Prod.map fcomp fcomp) id
⊢ map (UniformFun.phi α β) (map (Prod.map fcomp fcomp) 𝓐 ×ˢ map id ⊤) =
    map (UniformFun.phi α β) (map (Prod.map fcomp fcomp) 𝓐 ×ˢ ⊤)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ UniformContinuous (↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun)
[PROOFSTEP]
refine uniformContinuous_iff.mpr ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ uniformSpace α γ ≤ UniformSpace.comap (↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun) (uniformSpace α β)
[PROOFSTEP]
exact (UniformFun.mono (uniformContinuous_iff.mp hf)).trans_eq UniformFun.comap_eq
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : UniformInducing f
⊢ UniformInducing (↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun)
[PROOFSTEP]
constructor
[GOAL]
case comap_uniformity
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : UniformInducing f
⊢ comap (fun x => ((↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun) x.fst, (↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun) x.snd))
      (𝓤 (α →ᵤ β)) =
    𝓤 (α →ᵤ γ)
[PROOFSTEP]
replace hf : (𝓤 β).comap (Prod.map f f) = _ := hf.comap_uniformity
[GOAL]
case comap_uniformity
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : comap (Prod.map f f) (𝓤 β) = 𝓤 γ
⊢ comap (fun x => ((↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun) x.fst, (↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun) x.snd))
      (𝓤 (α →ᵤ β)) =
    𝓤 (α →ᵤ γ)
[PROOFSTEP]
change comap (Prod.map (ofFun ∘ (f ∘ ·) ∘ toFun) (ofFun ∘ (f ∘ ·) ∘ toFun)) _ = _
[GOAL]
case comap_uniformity
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : comap (Prod.map f f) (𝓤 β) = 𝓤 γ
⊢ comap (Prod.map (↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun) (↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun)) (𝓤 (α →ᵤ β)) = 𝓤 (α →ᵤ γ)
[PROOFSTEP]
rw [← uniformity_comap] at hf ⊢
[GOAL]
case comap_uniformity
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ 𝓤 (α →ᵤ γ) = 𝓤 (α →ᵤ γ)
[PROOFSTEP]
congr
[GOAL]
case comap_uniformity.h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ UniformSpace.comap (↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun) (uniformSpace α β) = uniformSpace α γ
[PROOFSTEP]
rw [← uniformSpace_eq hf, UniformFun.comap_eq]
[GOAL]
case comap_uniformity.h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ UniformSpace.comap (↑ofFun ∘ (fun x => f ∘ x) ∘ ↑toFun) (uniformSpace α β) =
    UniformSpace.comap (fun x => f ∘ x) (uniformSpace α β)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → α
⊢ UniformContinuous fun g => ↑ofFun (g ∘ f)
[PROOFSTEP]
rw [uniformContinuous_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → α
⊢ uniformSpace α β ≤ UniformSpace.comap (fun g => ↑ofFun (g ∘ f)) (uniformSpace γ β)
[PROOFSTEP]
change 𝓤 (α →ᵤ β) ≤ (𝓤 (γ →ᵤ β)).comap (Prod.map (fun g : α →ᵤ β => g ∘ f) fun g : α →ᵤ β => g ∘ f)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → α
⊢ 𝓤 (α →ᵤ β) ≤ comap (Prod.map (fun g => g ∘ f) fun g => g ∘ f) (𝓤 (γ →ᵤ β))
[PROOFSTEP]
rw [(UniformFun.hasBasis_uniformity α β).le_basis_iff ((UniformFun.hasBasis_uniformity γ β).comap _)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
f : γ → α
⊢ ∀ (i' : Set (β × β)),
    i' ∈ 𝓤 β →
      ∃ i, i ∈ 𝓤 β ∧ UniformFun.gen α β i ⊆ (Prod.map (fun g => g ∘ f) fun g => g ∘ f) ⁻¹' UniformFun.gen γ β i'
[PROOFSTEP]
exact fun U hU => ⟨U, hU, fun uv huv x => huv (f x)⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : T2Space β
⊢ ∀ (x y : α →ᵤ β), x ≠ y → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
[PROOFSTEP]
intro f g h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g✝ : ι → α
inst✝¹ : UniformSpace β
inst✝ : T2Space β
f g : α →ᵤ β
h : f ≠ g
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
obtain ⟨x, hx⟩ := not_forall.mp (mt funext h)
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x✝ : α
p : Filter ι
g✝ : ι → α
inst✝¹ : UniformSpace β
inst✝ : T2Space β
f g : α →ᵤ β
h : f ≠ g
x : α
hx : ¬f x = g x
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
exact separated_by_continuous (uniformContinuous_eval β x).continuous hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
⊢ UniformContinuous ↑toFun
[PROOFSTEP]
rw [uniformContinuous_pi]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
⊢ ∀ (i : α), UniformContinuous fun x => ↑toFun x i
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x✝ : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
x : α
⊢ UniformContinuous fun x_1 => ↑toFun x_1 x
[PROOFSTEP]
exact uniformContinuous_eval β x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
F : ι → α →ᵤ β
f : α →ᵤ β
⊢ Tendsto F p (𝓝 f) ↔ TendstoUniformly F f p
[PROOFSTEP]
rw [(UniformFun.hasBasis_nhds α β f).tendsto_right_iff, TendstoUniformly]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
F : ι → α →ᵤ β
f : α →ᵤ β
⊢ (∀ (i : Set (β × β)), i ∈ 𝓤 β → ∀ᶠ (x : ι) in p, F x ∈ {g | (f, g) ∈ UniformFun.gen α β i}) ↔
    ∀ (u : Set (β × β)), u ∈ 𝓤 β → ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ u
[PROOFSTEP]
exact Iff.rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ UniformInducing ↑(Equiv.arrowProdEquivProdArrow β γ α)
[PROOFSTEP]
constructor
[GOAL]
case comap_uniformity
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ comap (fun x => (↑(Equiv.arrowProdEquivProdArrow β γ α) x.fst, ↑(Equiv.arrowProdEquivProdArrow β γ α) x.snd))
      (𝓤 ((α →ᵤ β) × (α →ᵤ γ))) =
    𝓤 (α →ᵤ β × γ)
[PROOFSTEP]
change comap (Prod.map (Equiv.arrowProdEquivProdArrow _ _ _) (Equiv.arrowProdEquivProdArrow _ _ _)) _ = _
[GOAL]
case comap_uniformity
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ comap (Prod.map ↑(Equiv.arrowProdEquivProdArrow β γ α) ↑(Equiv.arrowProdEquivProdArrow β γ α))
      (𝓤 ((α →ᵤ β) × (α →ᵤ γ))) =
    𝓤 (α →ᵤ β × γ)
[PROOFSTEP]
simp_rw [UniformFun]
[GOAL]
case comap_uniformity
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ comap (Prod.map ↑(Equiv.arrowProdEquivProdArrow β γ α) ↑(Equiv.arrowProdEquivProdArrow β γ α))
      (𝓤 ((α → β) × (α → γ))) =
    𝓤 (α → β × γ)
[PROOFSTEP]
rw [← uniformity_comap]
[GOAL]
case comap_uniformity
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ 𝓤 (α → β × γ) = 𝓤 (α → β × γ)
[PROOFSTEP]
congr
[GOAL]
case comap_uniformity.h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ UniformSpace.comap (↑(Equiv.arrowProdEquivProdArrow β γ α)) instUniformSpaceProd = uniformSpace α (β × γ)
[PROOFSTEP]
unfold instUniformSpaceProd
[GOAL]
case comap_uniformity.h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ UniformSpace.comap (↑(Equiv.arrowProdEquivProdArrow β γ α))
      (UniformSpace.comap Prod.fst (uniformSpace α β) ⊓ UniformSpace.comap Prod.snd (uniformSpace α γ)) =
    uniformSpace α (β × γ)
[PROOFSTEP]
rw [UniformSpace.comap_inf, ← UniformSpace.comap_comap, ← UniformSpace.comap_comap]
[GOAL]
case comap_uniformity.h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ UniformSpace.comap (Prod.fst ∘ ↑(Equiv.arrowProdEquivProdArrow β γ α)) (uniformSpace α β) ⊓
      UniformSpace.comap (Prod.snd ∘ ↑(Equiv.arrowProdEquivProdArrow β γ α)) (uniformSpace α γ) =
    uniformSpace α (β × γ)
[PROOFSTEP]
have := (@UniformFun.inf_eq α (β × γ) (UniformSpace.comap Prod.fst ‹_›) (UniformSpace.comap Prod.snd ‹_›)).symm
[GOAL]
case comap_uniformity.h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
this : uniformSpace α (β × γ) ⊓ uniformSpace α (β × γ) = uniformSpace α (β × γ)
⊢ UniformSpace.comap (Prod.fst ∘ ↑(Equiv.arrowProdEquivProdArrow β γ α)) (uniformSpace α β) ⊓
      UniformSpace.comap (Prod.snd ∘ ↑(Equiv.arrowProdEquivProdArrow β γ α)) (uniformSpace α γ) =
    uniformSpace α (β × γ)
[PROOFSTEP]
rwa [UniformFun.comap_eq, UniformFun.comap_eq] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ UniformInducing ↑(Equiv.piComm fun a i => δ i)
[PROOFSTEP]
refine @UniformInducing.mk ?_ ?_ ?_ ?_ ?_ ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ comap (fun x => (↑(Equiv.piComm fun a i => δ i) x.fst, ↑(Equiv.piComm fun a i => δ i) x.snd))
      (𝓤 ((i : ι) → (fun i => α → δ i) i)) =
    𝓤 (α →ᵤ (i : ι) → δ i)
[PROOFSTEP]
change comap (Prod.map Function.swap Function.swap) _ = _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ comap (Prod.map Function.swap Function.swap) (𝓤 ((i : ι) → (fun i => α → δ i) i)) = 𝓤 (α →ᵤ (i : ι) → δ i)
[PROOFSTEP]
rw [← uniformity_comap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ 𝓤 (α → (y : ι) → δ y) = 𝓤 (α →ᵤ (i : ι) → δ i)
[PROOFSTEP]
congr
[GOAL]
case h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ UniformSpace.comap Function.swap (Pi.uniformSpace fun i => α → δ i) = uniformSpace α ((i : ι) → δ i)
[PROOFSTEP]
unfold Pi.uniformSpace
[GOAL]
case h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ UniformSpace.comap Function.swap
      (UniformSpace.ofCoreEq UniformSpace.toCore Pi.topologicalSpace
        (_ : Pi.topologicalSpace = UniformSpace.Core.toTopologicalSpace UniformSpace.toCore)) =
    uniformSpace α ((i : ι) → δ i)
[PROOFSTEP]
rw [UniformSpace.ofCoreEq_toCore, UniformSpace.ofCoreEq_toCore, UniformSpace.comap_iInf, UniformFun.iInf_eq]
[GOAL]
case h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ ⨅ (i : ι), UniformSpace.comap Function.swap (UniformSpace.comap (fun a => a i) ((fun i => uniformSpace α (δ i)) i)) =
    ⨅ (i : ι), uniformSpace α ((i : ι) → δ i)
[PROOFSTEP]
refine' iInf_congr fun i => _
[GOAL]
case h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
i : ι
⊢ UniformSpace.comap Function.swap (UniformSpace.comap (fun a => a i) ((fun i => uniformSpace α (δ i)) i)) =
    uniformSpace α ((i : ι) → δ i)
[PROOFSTEP]
rw [← UniformSpace.comap_comap, UniformFun.comap_eq]
[GOAL]
case h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
i : ι
⊢ UniformSpace.comap ((fun a => a i) ∘ Function.swap) ((fun i => uniformSpace α (δ i)) i) =
    UniformSpace.comap (fun x => (fun a => a i) ∘ x) (uniformSpace α (δ i))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
𝔖 : Set (Set α)
S : Set α
V : Set (β × β)
⊢ UniformOnFun.gen 𝔖 S V =
    Prod.map (restrict S ∘ ↑UniformFun.toFun) (restrict S ∘ ↑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β V
[PROOFSTEP]
ext uv
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
𝔖 : Set (Set α)
S : Set α
V : Set (β × β)
uv : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)
⊢ uv ∈ UniformOnFun.gen 𝔖 S V ↔
    uv ∈ Prod.map (restrict S ∘ ↑UniformFun.toFun) (restrict S ∘ ↑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β V
[PROOFSTEP]
exact ⟨fun h ⟨x, hx⟩ => h x hx, fun h x hx => h ⟨x, hx⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ topologicalSpace α β 𝔖 =
    ⨅ (s : Set α) (_ : s ∈ 𝔖),
      TopologicalSpace.induced (restrict s ∘ ↑UniformFun.toFun) (UniformFun.topologicalSpace (↑s) β)
[PROOFSTEP]
simp only [UniformOnFun.topologicalSpace, toTopologicalSpace_iInf, toTopologicalSpace_iInf, toTopologicalSpace_comap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ ⨅ (i : Set α) (_ : i ∈ 𝔖), TopologicalSpace.induced (restrict i) UniformSpace.toTopologicalSpace =
    ⨅ (s : Set α) (_ : s ∈ 𝔖),
      TopologicalSpace.induced (restrict s ∘ ↑UniformFun.toFun) (UniformFun.topologicalSpace (↑s) β)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ s' : Set α
x : α
p✝ : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
p : ι → Prop
s : ι → Set (β × β)
hb : HasBasis (𝓤 β) p s
S : Set α
⊢ HasBasis (𝓤 (α →ᵤ[𝔖] β)) p fun i => UniformOnFun.gen 𝔖 S (s i)
[PROOFSTEP]
simp_rw [UniformOnFun.gen_eq_preimage_restrict, uniformity_comap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ s' : Set α
x : α
p✝ : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
p : ι → Prop
s : ι → Set (β × β)
hb : HasBasis (𝓤 β) p s
S : Set α
⊢ HasBasis (comap (Prod.map (restrict S) (restrict S)) (𝓤 (↑S → β))) p fun i =>
    Prod.map (restrict S ∘ ↑UniformFun.toFun) (restrict S ∘ ↑UniformFun.toFun) ⁻¹' UniformFun.gen (↑S) β (s i)
[PROOFSTEP]
exact (UniformFun.hasBasis_uniformity_of_basis S β hb).comap _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ s' : Set α
x : α
p✝ : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : Set.Nonempty 𝔖
h' : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
p : ι → Prop
s : ι → Set (β × β)
hb : HasBasis (𝓤 β) p s
⊢ HasBasis (𝓤 (α →ᵤ[𝔖] β)) (fun Si => Si.fst ∈ 𝔖 ∧ p Si.snd) fun Si => UniformOnFun.gen 𝔖 Si.fst (s Si.snd)
[PROOFSTEP]
simp only [iInf_uniformity]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ s' : Set α
x : α
p✝ : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : Set.Nonempty 𝔖
h' : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖
p : ι → Prop
s : ι → Set (β × β)
hb : HasBasis (𝓤 β) p s
⊢ HasBasis (⨅ (i : Set α) (_ : i ∈ 𝔖), 𝓤 (α →ᵤ[𝔖] β)) (fun Si => Si.fst ∈ 𝔖 ∧ p Si.snd) fun Si =>
    UniformOnFun.gen 𝔖 Si.fst (s Si.snd)
[PROOFSTEP]
exact
  hasBasis_biInf_of_directed h (fun S => UniformOnFun.gen 𝔖 S ∘ s) _
    (fun S _hS => UniformOnFun.hasBasis_uniformity_of_basis_aux₁ α β 𝔖 hb S)
    (UniformOnFun.hasBasis_uniformity_of_basis_aux₂ α β 𝔖 h' hb)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : s ∈ 𝔖
⊢ UniformContinuous (↑UniformFun.ofFun ∘ restrict s ∘ ↑(toFun 𝔖))
[PROOFSTEP]
change _ ≤ _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : s ∈ 𝔖
⊢ map
      (fun x =>
        ((↑UniformFun.ofFun ∘ restrict s ∘ ↑(toFun 𝔖)) x.fst, (↑UniformFun.ofFun ∘ restrict s ∘ ↑(toFun 𝔖)) x.snd))
      (𝓤 (α →ᵤ[𝔖] β)) ≤
    𝓤 (↑s →ᵤ β)
[PROOFSTEP]
simp only [UniformOnFun.uniformSpace, map_le_iff_le_comap, iInf_uniformity]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : s ∈ 𝔖
⊢ ⨅ (i : Set α) (_ : i ∈ 𝔖), 𝓤 (α →ᵤ[𝔖] β) ≤
    comap
      (fun x =>
        ((↑UniformFun.ofFun ∘ restrict s ∘ ↑(toFun 𝔖)) x.fst, (↑UniformFun.ofFun ∘ restrict s ∘ ↑(toFun 𝔖)) x.snd))
      (𝓤 (↑s →ᵤ β))
[PROOFSTEP]
exact iInf₂_le s h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ uniformSpace α γ 𝔖 = ⨅ (i : ι), uniformSpace α γ 𝔖
[PROOFSTEP]
simp_rw [UniformOnFun.uniformSpace, UniformFun.iInf_eq, UniformSpace.comap_iInf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ ⨅ (s : Set α) (_ : s ∈ 𝔖) (i : ι), UniformSpace.comap (restrict s) (UniformFun.uniformSpace (↑s) γ) =
    ⨅ (i : ι) (s : Set α) (_ : s ∈ 𝔖), UniformSpace.comap (restrict s) (UniformFun.uniformSpace (↑s) γ)
[PROOFSTEP]
rw [iInf_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ ⨅ (s : Set α) (_ : s ∈ 𝔖) (i : ι), UniformSpace.comap (restrict s) (UniformFun.uniformSpace (↑s) γ) =
    ⨅ (j : Set α) (i : ι) (_ : j ∈ 𝔖), UniformSpace.comap (restrict j) (UniformFun.uniformSpace (↑j) γ)
[PROOFSTEP]
exact iInf_congr fun s => iInf_comm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
⊢ uniformSpace α γ 𝔖 = uniformSpace α γ 𝔖 ⊓ uniformSpace α γ 𝔖
[PROOFSTEP]
rw [inf_eq_iInf, inf_eq_iInf, UniformOnFun.iInf_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
⊢ ⨅ (i : Bool), uniformSpace α γ 𝔖 = ⨅ (b : Bool), bif b then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖
[PROOFSTEP]
refine' iInf_congr fun i => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
i : Bool
⊢ uniformSpace α γ 𝔖 = bif i then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖
[PROOFSTEP]
cases i
[GOAL]
case false
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
⊢ uniformSpace α γ 𝔖 = bif false then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖
[PROOFSTEP]
rfl
[GOAL]
case true
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
u₁ u₂ : UniformSpace γ
⊢ uniformSpace α γ 𝔖 = bif true then uniformSpace α γ 𝔖 else uniformSpace α γ 𝔖
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : γ → β
⊢ uniformSpace α γ 𝔖 = UniformSpace.comap ((fun x x_1 => x ∘ x_1) f) (uniformSpace α β 𝔖)
[PROOFSTEP]
simp_rw [UniformOnFun.uniformSpace, UniformSpace.comap_iInf, UniformFun.comap_eq, ← UniformSpace.comap_comap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : γ → β
⊢ ⨅ (s : Set α) (_ : s ∈ 𝔖), UniformSpace.comap ((fun x => f ∘ x) ∘ restrict s) (UniformFun.uniformSpace (↑s) β) =
    ⨅ (i : Set α) (_ : i ∈ 𝔖), UniformSpace.comap (restrict i ∘ fun x => f ∘ x) (UniformFun.uniformSpace (↑i) β)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ UniformContinuous (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖))
[PROOFSTEP]
rw [uniformContinuous_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : UniformContinuous f
⊢ uniformSpace α γ 𝔖 ≤ UniformSpace.comap (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)) (uniformSpace α β 𝔖)
[PROOFSTEP]
exact (UniformOnFun.mono (uniformContinuous_iff.mp hf) subset_rfl).trans_eq UniformOnFun.comap_eq
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : UniformInducing f
⊢ UniformInducing (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖))
[PROOFSTEP]
constructor
[GOAL]
case comap_uniformity
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : UniformInducing f
⊢ comap
      (fun x =>
        ((↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)) x.fst,
          (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)) x.snd))
      (𝓤 (α →ᵤ[𝔖] β)) =
    𝓤 (α →ᵤ[𝔖] γ)
[PROOFSTEP]
replace hf : (𝓤 β).comap (Prod.map f f) = _ := hf.comap_uniformity
[GOAL]
case comap_uniformity
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : comap (Prod.map f f) (𝓤 β) = 𝓤 γ
⊢ comap
      (fun x =>
        ((↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)) x.fst,
          (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)) x.snd))
      (𝓤 (α →ᵤ[𝔖] β)) =
    𝓤 (α →ᵤ[𝔖] γ)
[PROOFSTEP]
change comap (Prod.map (ofFun 𝔖 ∘ (· ∘ ·) f ∘ toFun 𝔖) (ofFun 𝔖 ∘ (· ∘ ·) f ∘ toFun 𝔖)) _ = _
[GOAL]
case comap_uniformity
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : comap (Prod.map f f) (𝓤 β) = 𝓤 γ
⊢ comap
      (Prod.map (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖))
        (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)))
      (𝓤 (α →ᵤ[𝔖] β)) =
    𝓤 (α →ᵤ[𝔖] γ)
[PROOFSTEP]
rw [← uniformity_comap] at hf ⊢
[GOAL]
case comap_uniformity
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ 𝓤 (α →ᵤ[𝔖] γ) = 𝓤 (α →ᵤ[𝔖] γ)
[PROOFSTEP]
congr
[GOAL]
case comap_uniformity.h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ UniformSpace.comap (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)) (uniformSpace α β 𝔖) = uniformSpace α γ 𝔖
[PROOFSTEP]
rw [← uniformSpace_eq hf, UniformOnFun.comap_eq]
[GOAL]
case comap_uniformity.h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ UniformSpace.comap (↑(ofFun 𝔖) ∘ (fun x x_1 => x ∘ x_1) f ∘ ↑(toFun 𝔖)) (uniformSpace α β 𝔖) =
    UniformSpace.comap ((fun x x_1 => x ∘ x_1) f) (uniformSpace α β 𝔖)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
⊢ UniformContinuous fun g => ↑(ofFun 𝔗) (g ∘ f)
[PROOFSTEP]
simp_rw [uniformContinuous_iff, UniformOnFun.uniformSpace, UniformSpace.comap_iInf, ← UniformSpace.comap_comap]
  -- For any `t ∈ 𝔗`, note `s := f '' t ∈ 𝔖`.
    -- We will show that `comap s.restrict 𝒰(↥s, β, uβ) ≤ comap (t.restrict ∘ (— ∘ f)) 𝒰(↥t, β, uβ)`.
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
⊢ ⨅ (s : Set α) (_ : s ∈ 𝔖), UniformSpace.comap (restrict s) (UniformFun.uniformSpace (↑s) β) ≤
    ⨅ (i : Set γ) (_ : i ∈ 𝔗),
      UniformSpace.comap (restrict i ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) (UniformFun.uniformSpace (↑i) β)
[PROOFSTEP]
refine'
  le_iInf₂ fun t ht =>
    iInf_le_of_le (f '' t) <|
      iInf_le_of_le (hf ht)
        _
          -- Let `f'` be the map from `t` to `f '' t` induced by `f`.
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
t : Set γ
ht : t ∈ 𝔗
⊢ UniformSpace.comap (restrict (f '' t)) (UniformFun.uniformSpace (↑(f '' t)) β) ≤
    UniformSpace.comap (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) (UniformFun.uniformSpace (↑t) β)
[PROOFSTEP]
let f' : t → f '' t :=
  (mapsTo_image f t).restrict f t
    (f '' t)
      -- By definition `t.restrict ∘ (— ∘ f) = (— ∘ f') ∘ (f '' t).restrict`.
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
t : Set γ
ht : t ∈ 𝔗
f' : ↑t → ↑(f '' t) := MapsTo.restrict f t (f '' t) (_ : MapsTo f t (f '' t))
⊢ UniformSpace.comap (restrict (f '' t)) (UniformFun.uniformSpace (↑(f '' t)) β) ≤
    UniformSpace.comap (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) (UniformFun.uniformSpace (↑t) β)
[PROOFSTEP]
have : (t.restrict ∘ fun g : α →ᵤ[𝔖] β => ofFun 𝔗 (g ∘ f)) = (fun g : f '' t → β => g ∘ f') ∘ (f '' t).restrict := rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
t : Set γ
ht : t ∈ 𝔗
f' : ↑t → ↑(f '' t) := MapsTo.restrict f t (f '' t) (_ : MapsTo f t (f '' t))
this : (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) = (fun g => g ∘ f') ∘ restrict (f '' t)
⊢ UniformSpace.comap (restrict (f '' t)) (UniformFun.uniformSpace (↑(f '' t)) β) ≤
    UniformSpace.comap (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) (UniformFun.uniformSpace (↑t) β)
[PROOFSTEP]
rw [this, @UniformSpace.comap_comap (α →ᵤ[𝔖] β) (f '' t →ᵤ β)]
  -- But this is exactly monotonicity of `comap` applied to
    -- `UniformFun.precomp_continuous`.
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
t : Set γ
ht : t ∈ 𝔗
f' : ↑t → ↑(f '' t) := MapsTo.restrict f t (f '' t) (_ : MapsTo f t (f '' t))
this : (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) = (fun g => g ∘ f') ∘ restrict (f '' t)
⊢ UniformSpace.comap (restrict (f '' t)) (UniformFun.uniformSpace (↑(f '' t)) β) ≤
    UniformSpace.comap (restrict (f '' t)) (UniformSpace.comap (fun g => g ∘ f') (UniformFun.uniformSpace (↑t) β))
[PROOFSTEP]
refine' UniformSpace.comap_mono _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
t : Set γ
ht : t ∈ 𝔗
f' : ↑t → ↑(f '' t) := MapsTo.restrict f t (f '' t) (_ : MapsTo f t (f '' t))
this : (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) = (fun g => g ∘ f') ∘ restrict (f '' t)
⊢ UniformFun.uniformSpace (↑(f '' t)) β ≤ UniformSpace.comap (fun g => g ∘ f') (UniformFun.uniformSpace (↑t) β)
[PROOFSTEP]
rw [← uniformContinuous_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : 𝔗 ⊆ image f ⁻¹' 𝔖
t : Set γ
ht : t ∈ 𝔗
f' : ↑t → ↑(f '' t) := MapsTo.restrict f t (f '' t) (_ : MapsTo f t (f '' t))
this : (restrict t ∘ fun g => ↑(ofFun 𝔗) (g ∘ f)) = (fun g => g ∘ f') ∘ restrict (f '' t)
⊢ UniformContinuous fun g => g ∘ f'
[PROOFSTEP]
exact UniformFun.precomp_uniformContinuous
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
e : γ ≃ α
he : 𝔗 ⊆ image ↑e ⁻¹' 𝔖
he' : 𝔖 ⊆ preimage ↑e ⁻¹' 𝔗
src✝ : (γ → β) ≃ (α → β) := Equiv.arrowCongr e (Equiv.refl β)
⊢ 𝔖 ⊆ (image fun x => ↑e.symm x) ⁻¹' 𝔗
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
e : γ ≃ α
he : 𝔗 ⊆ image ↑e ⁻¹' 𝔖
he' : 𝔖 ⊆ preimage ↑e ⁻¹' 𝔗
src✝ : (γ → β) ≃ (α → β) := Equiv.arrowCongr e (Equiv.refl β)
s : Set α
hs : s ∈ 𝔖
⊢ s ∈ (image fun x => ↑e.symm x) ⁻¹' 𝔗
[PROOFSTEP]
change e.symm '' s ∈ 𝔗
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
e : γ ≃ α
he : 𝔗 ⊆ image ↑e ⁻¹' 𝔖
he' : 𝔖 ⊆ preimage ↑e ⁻¹' 𝔗
src✝ : (γ → β) ≃ (α → β) := Equiv.arrowCongr e (Equiv.refl β)
s : Set α
hs : s ∈ 𝔖
⊢ ↑e.symm '' s ∈ 𝔗
[PROOFSTEP]
rw [← preimage_equiv_eq_image_symm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
e : γ ≃ α
he : 𝔗 ⊆ image ↑e ⁻¹' 𝔖
he' : 𝔖 ⊆ preimage ↑e ⁻¹' 𝔗
src✝ : (γ → β) ≃ (α → β) := Equiv.arrowCongr e (Equiv.refl β)
s : Set α
hs : s ∈ 𝔖
⊢ ↑e ⁻¹' s ∈ 𝔗
[PROOFSTEP]
exact he' hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : T2Space β
h : ⋃₀ 𝔖 = univ
⊢ ∀ (x y : α →ᵤ[𝔖] β), x ≠ y → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
[PROOFSTEP]
intro f g hfg
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g✝ : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
obtain ⟨x, hx⟩ := not_forall.mp (mt funext hfg)
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x✝ : α
p : Filter ι
g✝ : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
x : α
hx : ¬f x = g x
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
obtain ⟨s, hs, hxs⟩ : ∃ s ∈ 𝔖, x ∈ s := mem_sUnion.mp (h.symm ▸ True.intro)
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ s' : Set α
x✝ : α
p : Filter ι
g✝ : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
x : α
hx : ¬f x = g x
s : Set α
hs : s ∈ 𝔖
hxs : x ∈ s
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
[PROOFSTEP]
exact separated_by_continuous (uniformContinuous_eval_of_mem β 𝔖 hxs hs).continuous hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
⊢ UniformContinuous ↑(toFun 𝔖)
[PROOFSTEP]
rw [uniformContinuous_pi]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
⊢ ∀ (i : α), UniformContinuous fun x => ↑(toFun 𝔖) x i
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x✝ : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
x : α
⊢ UniformContinuous fun x_1 => ↑(toFun 𝔖) x_1 x
[PROOFSTEP]
obtain ⟨s : Set α, hs : s ∈ 𝔖, hxs : x ∈ s⟩ := sUnion_eq_univ_iff.mp h x
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ s' : Set α
x✝ : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
x : α
s : Set α
hs : s ∈ 𝔖
hxs : x ∈ s
⊢ UniformContinuous fun x_1 => ↑(toFun 𝔖) x_1 x
[PROOFSTEP]
exact uniformContinuous_eval_of_mem β 𝔖 hxs hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
⊢ Tendsto F p (𝓝 f) ↔ ∀ (s : Set α), s ∈ 𝔖 → TendstoUniformlyOn F f p s
[PROOFSTEP]
rw [UniformOnFun.topologicalSpace_eq, nhds_iInf, tendsto_iInf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
⊢ (∀ (i : Set α), Tendsto F p (𝓝 f)) ↔ ∀ (s : Set α), s ∈ 𝔖 → TendstoUniformlyOn F f p s
[PROOFSTEP]
refine' forall_congr' fun s => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
s : Set α
⊢ Tendsto F p (𝓝 f) ↔ s ∈ 𝔖 → TendstoUniformlyOn F f p s
[PROOFSTEP]
rw [nhds_iInf, tendsto_iInf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
s : Set α
⊢ s ∈ 𝔖 → Tendsto F p (𝓝 f) ↔ s ∈ 𝔖 → TendstoUniformlyOn F f p s
[PROOFSTEP]
refine' forall_congr' fun hs => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
s : Set α
hs : s ∈ 𝔖
⊢ Tendsto F p (𝓝 f) ↔ TendstoUniformlyOn F f p s
[PROOFSTEP]
rw [nhds_induced (T := _), tendsto_comap_iff, tendstoUniformlyOn_iff_tendstoUniformly_comp_coe,
  UniformFun.tendsto_iff_tendstoUniformly]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
s : Set α
hs : s ∈ 𝔖
⊢ TendstoUniformly ((restrict s ∘ ↑UniformFun.toFun) ∘ F) ((restrict s ∘ ↑UniformFun.toFun) f) p ↔
    TendstoUniformly (fun i x => F i ↑x) (f ∘ Subtype.val) p
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
⊢ UniformInducing
    ↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
[PROOFSTEP]
constructor
[GOAL]
case comap_uniformity
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
⊢ comap
      (fun x =>
        (↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
            x.fst,
          ↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
            x.snd))
      (𝓤 ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] γ))) =
    𝓤 (α →ᵤ[𝔖] β × γ)
[PROOFSTEP]
rw [uniformity_prod, comap_inf, comap_comap, comap_comap]
[GOAL]
case comap_uniformity
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
⊢ comap
        ((fun p => (p.fst.fst, p.snd.fst)) ∘ fun x =>
          (↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.fst,
            ↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.snd))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p => (p.fst.snd, p.snd.snd)) ∘ fun x =>
          (↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.fst,
            ↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.snd))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    𝓤 (α →ᵤ[𝔖] β × γ)
[PROOFSTEP]
have H := @UniformOnFun.inf_eq α (β × γ) 𝔖 (UniformSpace.comap Prod.fst ‹_›) (UniformSpace.comap Prod.snd ‹_›)
[GOAL]
case comap_uniformity
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
H : uniformSpace α (β × γ) 𝔖 = uniformSpace α (β × γ) 𝔖 ⊓ uniformSpace α (β × γ) 𝔖
⊢ comap
        ((fun p => (p.fst.fst, p.snd.fst)) ∘ fun x =>
          (↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.fst,
            ↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.snd))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p => (p.fst.snd, p.snd.snd)) ∘ fun x =>
          (↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.fst,
            ↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.snd))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    𝓤 (α →ᵤ[𝔖] β × γ)
[PROOFSTEP]
apply_fun (fun u ↦ @uniformity (α →ᵤ[𝔖] β × γ) u) at H 
[GOAL]
case comap_uniformity
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
H : 𝓤 (α →ᵤ[𝔖] β × γ) = 𝓤 (α →ᵤ[𝔖] β × γ)
⊢ comap
        ((fun p => (p.fst.fst, p.snd.fst)) ∘ fun x =>
          (↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.fst,
            ↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.snd))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p => (p.fst.snd, p.snd.snd)) ∘ fun x =>
          (↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.fst,
            ↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.snd))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    𝓤 (α →ᵤ[𝔖] β × γ)
[PROOFSTEP]
convert H.symm using 1
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
H : 𝓤 (α →ᵤ[𝔖] β × γ) = 𝓤 (α →ᵤ[𝔖] β × γ)
⊢ comap
        ((fun p => (p.fst.fst, p.snd.fst)) ∘ fun x =>
          (↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.fst,
            ↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.snd))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p => (p.fst.snd, p.snd.snd)) ∘ fun x =>
          (↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.fst,
            ↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.snd))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    𝓤 (α →ᵤ[𝔖] β × γ)
[PROOFSTEP]
rw [UniformOnFun.comap_eq, UniformOnFun.comap_eq]
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
H : 𝓤 (α →ᵤ[𝔖] β × γ) = 𝓤 (α →ᵤ[𝔖] β × γ)
⊢ comap
        ((fun p => (p.fst.fst, p.snd.fst)) ∘ fun x =>
          (↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.fst,
            ↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.snd))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p => (p.fst.snd, p.snd.snd)) ∘ fun x =>
          (↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.fst,
            ↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.snd))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    𝓤 (α →ᵤ[𝔖] β × γ)
[PROOFSTEP]
erw [inf_uniformity]
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
H : 𝓤 (α →ᵤ[𝔖] β × γ) = 𝓤 (α →ᵤ[𝔖] β × γ)
⊢ comap
        ((fun p => (p.fst.fst, p.snd.fst)) ∘ fun x =>
          (↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.fst,
            ↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.snd))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p => (p.fst.snd, p.snd.snd)) ∘ fun x =>
          (↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.fst,
            ↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.snd))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    𝓤 (α →ᵤ[𝔖] β × γ) ⊓ 𝓤 (α →ᵤ[𝔖] β × γ)
[PROOFSTEP]
rw [uniformity_comap, uniformity_comap]
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
H : 𝓤 (α →ᵤ[𝔖] β × γ) = 𝓤 (α →ᵤ[𝔖] β × γ)
⊢ comap
        ((fun p => (p.fst.fst, p.snd.fst)) ∘ fun x =>
          (↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.fst,
            ↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.snd))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p => (p.fst.snd, p.snd.snd)) ∘ fun x =>
          (↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.fst,
            ↑((ofFun 𝔖).symm.trans ((Equiv.arrowProdEquivProdArrow β γ α).trans (Equiv.prodCongr (ofFun 𝔖) (ofFun 𝔖))))
              x.snd))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    comap (Prod.map ((fun x x_1 => x ∘ x_1) Prod.fst) ((fun x x_1 => x ∘ x_1) Prod.fst)) (𝓤 (α → β)) ⊓
      comap (Prod.map ((fun x x_1 => x ∘ x_1) Prod.snd) ((fun x x_1 => x ∘ x_1) Prod.snd)) (𝓤 (α → γ))
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ UniformInducing ↑(Equiv.piComm fun a i => δ i)
[PROOFSTEP]
constructor
[GOAL]
case comap_uniformity
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ comap (fun x => (↑(Equiv.piComm fun a i => δ i) x.fst, ↑(Equiv.piComm fun a i => δ i) x.snd))
      (𝓤 ((i : ι) → α →ᵤ[𝔖] δ i)) =
    𝓤 (α →ᵤ[𝔖] (i : ι) → δ i)
[PROOFSTEP]
change comap (Prod.map Function.swap Function.swap) _ = _
[GOAL]
case comap_uniformity
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ comap (Prod.map Function.swap Function.swap) (𝓤 ((i : ι) → α →ᵤ[𝔖] δ i)) = 𝓤 (α →ᵤ[𝔖] (i : ι) → δ i)
[PROOFSTEP]
erw [← uniformity_comap]
[GOAL]
case comap_uniformity
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ 𝓤 (α → (y : ι) → δ y) = 𝓤 (α →ᵤ[𝔖] (i : ι) → δ i)
[PROOFSTEP]
congr
[GOAL]
case comap_uniformity.h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ UniformSpace.comap Function.swap (Pi.uniformSpace fun i => α →ᵤ[𝔖] δ i) = uniformSpace α ((i : ι) → δ i) 𝔖
[PROOFSTEP]
rw [Pi.uniformSpace, UniformSpace.ofCoreEq_toCore, Pi.uniformSpace, UniformSpace.ofCoreEq_toCore,
  UniformSpace.comap_iInf, UniformOnFun.iInf_eq]
[GOAL]
case comap_uniformity.h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
⊢ ⨅ (i : ι), UniformSpace.comap Function.swap (UniformSpace.comap (fun a => a i) (uniformSpace α (δ i) 𝔖)) =
    ⨅ (i : ι), uniformSpace α ((i : ι) → δ i) 𝔖
[PROOFSTEP]
refine' iInf_congr fun i => _
[GOAL]
case comap_uniformity.h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
i : ι
⊢ UniformSpace.comap Function.swap (UniformSpace.comap (fun a => a i) (uniformSpace α (δ i) 𝔖)) =
    uniformSpace α ((i : ι) → δ i) 𝔖
[PROOFSTEP]
rw [← UniformSpace.comap_comap, UniformOnFun.comap_eq]
[GOAL]
case comap_uniformity.h.e_2.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst✝ : (i : ι) → UniformSpace (δ i)
i : ι
⊢ UniformSpace.comap ((fun a => a i) ∘ Function.swap) (uniformSpace α (δ i) 𝔖) =
    UniformSpace.comap ((fun x x_1 => x ∘ x_1) fun a => a i) (uniformSpace α (δ i) 𝔖)
[PROOFSTEP]
rfl
