ι : Sort ?u.18874
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
r : ℝ≥0∞
h : r < infEdist x s
⊢ ∀ ⦃a : α⦄, a ∈ closedBall x r → ¬a ∈ s
ι : Sort ?u.18874
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
r : ℝ≥0∞
h : r < infEdist x s
⊢ Disjoint (closedBall x r) s
rw [disjoint_left]
ι : Sort ?u.18874
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y✝ : α
s t : Set α
Φ : α → β
r : ℝ≥0∞
h : r < infEdist x s
y : α
hy : y ∈ closedBall x r
h'y : y ∈ s
⊢ False
ι : Sort ?u.18874
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : α
s t : Set α
Φ : α → β
r : ℝ≥0∞
h : r < infEdist x s
⊢ ∀ ⦃a : α⦄, a ∈ closedBall x r → ¬a ∈ s
intro y hy h'y
ι : Sort ?u.18874
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y✝ : α
s t : Set α
Φ : α → β
r : ℝ≥0∞
h : r < infEdist x s
y : α
hy : y ∈ closedBall x r
h'y : y ∈ s
⊢ infEdist x s < infEdist x s
ι : Sort ?u.18874
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y✝ : α
s t : Set α
Φ : α → β
r : ℝ≥0∞
h : r < infEdist x s
y : α
hy : y ∈ closedBall x r
h'y : y ∈ s
⊢ False
apply lt_irrefl (infEdist x s)
no goals
ι : Sort ?u.18874
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y✝ : α
s t : Set α
Φ : α → β
r : ℝ≥0∞
h : r < infEdist x s
y : α
hy : y ∈ closedBall x r
h'y : y ∈ s
⊢ infEdist x s < infEdist x s
calc
  infEdist x s ≤ edist x y := infEdist_le_edist_of_mem h'y
  _ ≤ r := by rwa [mem_closedBall, edist_comm] at hy
  _ < infEdist x s := h
no goals
ι : Sort ?u.18874
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y✝ : α
s t : Set α
Φ : α → β
r : ℝ≥0∞
h : r < infEdist x s
y : α
hy : y ∈ closedBall x r
h'y : y ∈ s
⊢ edist x y ≤ r
rwa [mem_closedBall, edist_comm] at hy