case h.dist.h.h
α✝ : Type u
β : Type v
X : Type ?u.169890
ι : Type ?u.169893
inst✝ : PseudoMetricSpace α✝
α : Type u_1
m : PseudoMetricSpace α
B : Bornology α
H : ∀ (s : Set α), IsBounded s ↔ IsBounded s
x✝¹ x✝ : α
⊢ dist x✝¹ x✝ = dist x✝¹ x✝
α✝ : Type u
β : Type v
X : Type ?u.169890
ι : Type ?u.169893
inst✝ : PseudoMetricSpace α✝
α : Type u_1
m : PseudoMetricSpace α
B : Bornology α
H : ∀ (s : Set α), IsBounded s ↔ IsBounded s
⊢ replaceBornology m H = m
ext
no goals
case h.dist.h.h
α✝ : Type u
β : Type v
X : Type ?u.169890
ι : Type ?u.169893
inst✝ : PseudoMetricSpace α✝
α : Type u_1
m : PseudoMetricSpace α
B : Bornology α
H : ∀ (s : Set α), IsBounded s ↔ IsBounded s
x✝¹ x✝ : α
⊢ dist x✝¹ x✝ = dist x✝¹ x✝
rfl