no goals
ι : Sort ?u.10627
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
⊢ 1 ≠ ⊤
simp
no goals
ι : Sort ?u.10627
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
⊢ ∀ (x y : α), infEdist x s ≤ infEdist y s + 1 * edist x y
simp only [one_mul, infEdist_le_infEdist_add_edist, forall₂_true_iff]