α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
⊢ indicator E (fun x => 1) a ≤ ↑(thickenedIndicator δ_pos E) a
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ (indicator E fun x => 1) ≤ ↑(thickenedIndicator δ_pos E)
intro a
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
h : a ∈ E
⊢ indicator E (fun x => 1) a ≤ ↑(thickenedIndicator δ_pos E) a

case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
h : ¬a ∈ E
⊢ indicator E (fun x => 1) a ≤ ↑(thickenedIndicator δ_pos E) a
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
⊢ indicator E (fun x => 1) a ≤ ↑(thickenedIndicator δ_pos E) a
by_cases a ∈ E
no goals
case pos
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
h : a ∈ E
⊢ indicator E (fun x => 1) a ≤ ↑(thickenedIndicator δ_pos E) a
simp only [h, indicator_of_mem, thickenedIndicator_one δ_pos E h, le_refl]
no goals
case neg
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
h : ¬a ∈ E
⊢ indicator E (fun x => 1) a ≤ ↑(thickenedIndicator δ_pos E) a
simp only [h, indicator_of_not_mem, not_false_iff, zero_le]