p : ℝ≥0∞
𝕜 : Type ?u.66094
𝕜' : Type ?u.66097
ι : Type u_1
α : ι → Type ?u.66105
β : ι → Type u_2
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
A : UniformInducing ↑(PiLp.equiv p β)
⊢ 𝓤 (PiLp p β) = 𝓤 ((i : ι) → β i)
p : ℝ≥0∞
𝕜 : Type ?u.66094
𝕜' : Type ?u.66097
ι : Type u_1
α : ι → Type ?u.66105
β : ι → Type u_2
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
⊢ 𝓤 (PiLp p β) = 𝓤 ((i : ι) → β i)
have A : UniformInducing (PiLp.equiv p β) :=
  (antilipschitzWith_equiv_aux p β).uniformInducing
    (lipschitzWith_equiv_aux p β).uniformContinuous
p : ℝ≥0∞
𝕜 : Type ?u.66094
𝕜' : Type ?u.66097
ι : Type u_1
α : ι → Type ?u.66105
β : ι → Type u_2
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
A : UniformInducing ↑(PiLp.equiv p β)
this : (fun x => (↑(PiLp.equiv p β) x.fst, ↑(PiLp.equiv p β) x.snd)) = id
⊢ 𝓤 (PiLp p β) = 𝓤 ((i : ι) → β i)
p : ℝ≥0∞
𝕜 : Type ?u.66094
𝕜' : Type ?u.66097
ι : Type u_1
α : ι → Type ?u.66105
β : ι → Type u_2
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
A : UniformInducing ↑(PiLp.equiv p β)
⊢ 𝓤 (PiLp p β) = 𝓤 ((i : ι) → β i)
have : (fun x : PiLp p β × PiLp p β => ((PiLp.equiv p β) x.fst, (PiLp.equiv p β) x.snd)) = id :=
  by ext i <;> rfl
no goals
p : ℝ≥0∞
𝕜 : Type ?u.66094
𝕜' : Type ?u.66097
ι : Type u_1
α : ι → Type ?u.66105
β : ι → Type u_2
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
A : UniformInducing ↑(PiLp.equiv p β)
this : (fun x => (↑(PiLp.equiv p β) x.fst, ↑(PiLp.equiv p β) x.snd)) = id
⊢ 𝓤 (PiLp p β) = 𝓤 ((i : ι) → β i)
rw [← A.comap_uniformity, this, comap_id]
no goals
p : ℝ≥0∞
𝕜 : Type ?u.66094
𝕜' : Type ?u.66097
ι : Type u_1
α : ι → Type ?u.66105
β : ι → Type u_2
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
A : UniformInducing ↑(PiLp.equiv p β)
⊢ (fun x => (↑(PiLp.equiv p β) x.fst, ↑(PiLp.equiv p β) x.snd)) = id
ext i <;> rfl