α : Type u_1
β : Type u_2
E : Type ?u.908
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
⊢ ∀ (s : Set (C(α, β) × C(α, β))),
    (∃ i,
        (IsCompact i.fst ∧ ∃ i_1, 0 < i_1 ∧ {p | dist p.fst p.snd ≤ i_1} ⊆ i.snd) ∧
          {fg | ∀ (x : α), x ∈ i.fst → (↑fg.fst x, ↑fg.snd x) ∈ i.snd} ⊆ s) ↔
      ∃ t,
        (∃ i, 0 < i ∧ {p | dist p.fst p.snd ≤ i} ⊆ t) ∧
          ∀ (x y : C(α, β)), (↑(equivBoundedOfCompact α β) x, ↑(equivBoundedOfCompact α β) y) ∈ t → (x, y) ∈ s
α : Type u_1
β : Type u_2
E : Type ?u.908
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
⊢ ∀ (s : Set (C(α, β) × C(α, β))),
    s ∈ uniformity C(α, β) ↔
      ∃ t,
        t ∈ uniformity (α →ᵇ β) ∧
          ∀ (x y : C(α, β)), (↑(equivBoundedOfCompact α β) x, ↑(equivBoundedOfCompact α β) y) ∈ t → (x, y) ∈ s
simp only [hasBasis_compactConvergenceUniformity.mem_iff, uniformity_basis_dist_le.mem_iff]
no goals
α : Type u_1
β : Type u_2
E : Type ?u.908
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : MetricSpace β
inst✝ : NormedAddCommGroup E
⊢ ∀ (s : Set (C(α, β) × C(α, β))),
    (∃ i,
        (IsCompact i.fst ∧ ∃ i_1, 0 < i_1 ∧ {p | dist p.fst p.snd ≤ i_1} ⊆ i.snd) ∧
          {fg | ∀ (x : α), x ∈ i.fst → (↑fg.fst x, ↑fg.snd x) ∈ i.snd} ⊆ s) ↔
      ∃ t,
        (∃ i, 0 < i ∧ {p | dist p.fst p.snd ≤ i} ⊆ t) ∧
          ∀ (x y : C(α, β)), (↑(equivBoundedOfCompact α β) x, ↑(equivBoundedOfCompact α β) y) ∈ t → (x, y) ∈ s
exact fun s =>
  ⟨fun ⟨⟨a, b⟩, ⟨_, ⟨ε, hε, hb⟩⟩, hs⟩ =>
    ⟨{ p | ∀ x, (p.1 x, p.2 x) ∈ b }, ⟨ε, hε, fun _ h x => hb ((dist_le hε.le).mp h x)⟩,
      fun f g h => hs fun x _ => h x⟩,
    fun ⟨_, ⟨ε, hε, ht⟩, hs⟩ =>
    ⟨⟨Set.univ, { p | dist p.1 p.2 ≤ ε }⟩, ⟨isCompact_univ, ⟨ε, hε, fun _ h => h⟩⟩,
      fun ⟨f, g⟩ h => hs _ _ (ht ((dist_le hε.le).mpr fun x => h x (mem_univ x)))⟩⟩