case a
α : Type u
β : Type v
X : Type ?u.203876
ι : Type ?u.203879
inst✝ : PseudoMetricSpace α
s : Set (α × α)
⊢ s ∈ 𝓤 α ↔ s ∈ comap (fun p => dist p.fst p.snd) (𝓝 0)
α : Type u
β : Type v
X : Type ?u.203876
ι : Type ?u.203879
inst✝ : PseudoMetricSpace α
⊢ 𝓤 α = comap (fun p => dist p.fst p.snd) (𝓝 0)
ext s
case a
α : Type u
β : Type v
X : Type ?u.203876
ι : Type ?u.203879
inst✝ : PseudoMetricSpace α
s : Set (α × α)
⊢ (∃ ε, ε > 0 ∧ ∀ {a b : α}, dist a b < ε → (a, b) ∈ s) ↔ ∃ i, 0 < i ∧ (fun p => dist p.fst p.snd) ⁻¹' ball 0 i ⊆ s
case a
α : Type u
β : Type v
X : Type ?u.203876
ι : Type ?u.203879
inst✝ : PseudoMetricSpace α
s : Set (α × α)
⊢ s ∈ 𝓤 α ↔ s ∈ comap (fun p => dist p.fst p.snd) (𝓝 0)
simp only [mem_uniformity_dist, (nhds_basis_ball.comap _).mem_iff]
no goals
case a
α : Type u
β : Type v
X : Type ?u.203876
ι : Type ?u.203879
inst✝ : PseudoMetricSpace α
s : Set (α × α)
⊢ (∃ ε, ε > 0 ∧ ∀ {a b : α}, dist a b < ε → (a, b) ∈ s) ↔ ∃ i, 0 < i ∧ (fun p => dist p.fst p.snd) ⁻¹' ball 0 i ⊆ s
simp [subset_def, Real.dist_0_eq_abs]