α : Type u_1
β : Type ?u.20
γ : Type ?u.23
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompactSpace α
⊢ 𝓤 α ≤ 𝓝ˢ (diagonal α)
α : Type u_1
β : Type ?u.20
γ : Type ?u.23
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompactSpace α
⊢ 𝓝ˢ (diagonal α) = 𝓤 α
refine' nhdsSet_diagonal_le_uniformity.antisymm _
α : Type u_1
β : Type ?u.20
γ : Type ?u.23
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompactSpace α
this :
  HasBasis (𝓤 (α × α)) (fun U => U ∈ 𝓤 α) fun U => (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹' U ×ˢ U
⊢ 𝓤 α ≤ 𝓝ˢ (diagonal α)
α : Type u_1
β : Type ?u.20
γ : Type ?u.23
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompactSpace α
⊢ 𝓤 α ≤ 𝓝ˢ (diagonal α)
have :
  (𝓤 (α × α)).HasBasis (fun U => U ∈ 𝓤 α) fun U =>
    (fun p : (α × α) × α × α => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U := by
  rw [uniformity_prod_eq_comap_prod]
  exact (𝓤 α).basis_sets.prod_self.comap _
α : Type u_1
β : Type ?u.20
γ : Type ?u.23
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompactSpace α
this :
  HasBasis (𝓤 (α × α)) (fun U => U ∈ 𝓤 α) fun U => (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹' U ×ˢ U
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ (⋃ (x : α × α) (_ : x ∈ diagonal α), ball x ((fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹' U ×ˢ U)) ∈
    𝓤 α
α : Type u_1
β : Type ?u.20
γ : Type ?u.23
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompactSpace α
this :
  HasBasis (𝓤 (α × α)) (fun U => U ∈ 𝓤 α) fun U => (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹' U ×ˢ U
⊢ 𝓤 α ≤ 𝓝ˢ (diagonal α)
refine' (isCompact_diagonal.nhdsSet_basis_uniformity this).ge_iff.2 fun U hU => _
no goals
α : Type u_1
β : Type ?u.20
γ : Type ?u.23
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompactSpace α
this :
  HasBasis (𝓤 (α × α)) (fun U => U ∈ 𝓤 α) fun U => (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹' U ×ˢ U
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ (⋃ (x : α × α) (_ : x ∈ diagonal α), ball x ((fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹' U ×ˢ U)) ∈
    𝓤 α
exact mem_of_superset hU fun ⟨x, y⟩ hxy => mem_iUnion₂.2
  ⟨(x, x), rfl, refl_mem_uniformity hU, hxy⟩
α : Type u_1
β : Type ?u.20
γ : Type ?u.23
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompactSpace α
⊢ HasBasis (Filter.comap (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) (𝓤 α ×ˢ 𝓤 α)) (fun U => U ∈ 𝓤 α)
    fun U => (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹' U ×ˢ U
α : Type u_1
β : Type ?u.20
γ : Type ?u.23
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompactSpace α
⊢ HasBasis (𝓤 (α × α)) (fun U => U ∈ 𝓤 α) fun U => (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹' U ×ˢ U
rw [uniformity_prod_eq_comap_prod]
no goals
α : Type u_1
β : Type ?u.20
γ : Type ?u.23
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompactSpace α
⊢ HasBasis (Filter.comap (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) (𝓤 α ×ˢ 𝓤 α)) (fun U => U ∈ 𝓤 α)
    fun U => (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) ⁻¹' U ×ˢ U
exact (𝓤 α).basis_sets.prod_self.comap _