α : Type u_1
inst✝ : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
x : α
⊢ ↑(thickenedIndicator δ₁_pos E) x ≤ ↑(thickenedIndicator δ₂_pos E) x
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
⊢ ↑(thickenedIndicator δ₁_pos E) ≤ ↑(thickenedIndicator δ₂_pos E)
intro x
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
x : α
⊢ thickenedIndicatorAux δ₁ E x ≤ thickenedIndicatorAux δ₂ E x
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
x : α
⊢ ↑(thickenedIndicator δ₁_pos E) x ≤ ↑(thickenedIndicator δ₂_pos E) x
apply (toNNReal_le_toNNReal thickenedIndicatorAux_lt_top.ne thickenedIndicatorAux_lt_top.ne).mpr
no goals
α : Type u_1
inst✝ : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
x : α
⊢ thickenedIndicatorAux δ₁ E x ≤ thickenedIndicatorAux δ₂ E x
apply thickenedIndicatorAux_mono hle