α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
⊢ thickenedIndicatorAux δ E x = 0
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ¬x ∈ thickening δ E
⊢ thickenedIndicatorAux δ E x = 0
rw [thickening, mem_setOf_eq, not_lt] at x_out
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
⊢ 1 - infEdist x E / ENNReal.ofReal δ = 0
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
⊢ thickenedIndicatorAux δ E x = 0
unfold thickenedIndicatorAux
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
⊢ 1 - infEdist x E / ENNReal.ofReal δ ≤ ⊥
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
⊢ 1 - infEdist x E / ENNReal.ofReal δ = 0
apply le_antisymm _ bot_le
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
key : 1 - infEdist x E / ENNReal.ofReal δ ≤ 1 - ENNReal.ofReal δ / ENNReal.ofReal δ
⊢ 1 - infEdist x E / ENNReal.ofReal δ ≤ ⊥
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
⊢ 1 - infEdist x E / ENNReal.ofReal δ ≤ ⊥
have key := tsub_le_tsub
  (@rfl _ (1 : ℝ≥0∞)).le (ENNReal.div_le_div x_out (@rfl _ (ENNReal.ofReal δ : ℝ≥0∞)).le)
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
key : 1 - infEdist x E / ENNReal.ofReal δ ≤ 1 - 1
⊢ 1 - infEdist x E / ENNReal.ofReal δ ≤ ⊥
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
key : 1 - infEdist x E / ENNReal.ofReal δ ≤ 1 - ENNReal.ofReal δ / ENNReal.ofReal δ
⊢ 1 - infEdist x E / ENNReal.ofReal δ ≤ ⊥
rw [ENNReal.div_self (ne_of_gt (ENNReal.ofReal_pos.mpr δ_pos)) ofReal_ne_top] at key
no goals
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEdist x E
key : 1 - infEdist x E / ENNReal.ofReal δ ≤ 1 - 1
⊢ 1 - infEdist x E / ENNReal.ofReal δ ≤ ⊥
simpa using key