α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : Tendsto (fun n => thickenedIndicatorAux (δseq n) E) atTop (𝓝 (indicator (closure E) fun x => 1))
⊢ Tendsto (fun n => ↑(thickenedIndicator (_ : 0 < δseq n) E)) atTop (𝓝 (indicator (closure E) fun x => 1))
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
⊢ Tendsto (fun n => ↑(thickenedIndicator (_ : 0 < δseq n) E)) atTop (𝓝 (indicator (closure E) fun x => 1))
have key := thickenedIndicatorAux_tendsto_indicator_closure δseq_lim E
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
⊢ ∀ (x : α),
    Tendsto (fun i => ↑(thickenedIndicator (_ : 0 < δseq i) E) x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : Tendsto (fun n => thickenedIndicatorAux (δseq n) E) atTop (𝓝 (indicator (closure E) fun x => 1))
⊢ Tendsto (fun n => ↑(thickenedIndicator (_ : 0 < δseq n) E)) atTop (𝓝 (indicator (closure E) fun x => 1))
rw [tendsto_pi_nhds] at *
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
x : α
⊢ Tendsto (fun i => ↑(thickenedIndicator (_ : 0 < δseq i) E) x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
⊢ ∀ (x : α),
    Tendsto (fun i => ↑(thickenedIndicator (_ : 0 < δseq i) E) x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
intro x
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
x : α
⊢ Tendsto (fun i => ↑(thickenedIndicator (_ : 0 < δseq i) E) x) atTop
    (𝓝 (ENNReal.toNNReal (indicator (closure E) (fun x => 1) x)))
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
x : α
⊢ Tendsto (fun i => ↑(thickenedIndicator (_ : 0 < δseq i) E) x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
rw [show indicator (closure E) (fun _ => (1 : ℝ≥0)) x =
      (indicator (closure E) (fun _ => (1 : ℝ≥0∞)) x).toNNReal
    by refine' (congr_fun (comp_indicator_const 1 ENNReal.toNNReal zero_toNNReal) x).symm]
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
x : α
⊢ indicator (closure E) (fun x => 1) x ≠ ⊤
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
x : α
⊢ Tendsto (fun i => ↑(thickenedIndicator (_ : 0 < δseq i) E) x) atTop
    (𝓝 (ENNReal.toNNReal (indicator (closure E) (fun x => 1) x)))
refine' Tendsto.comp (tendsto_toNNReal _) (key x)
no goals
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
x : α
⊢ indicator (closure E) (fun x => 1) x ≠ ⊤
by_cases x_mem : x ∈ closure E <;> simp [x_mem]
no goals
α : Type u_1
inst✝ : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key : ∀ (x : α), Tendsto (fun i => thickenedIndicatorAux (δseq i) E x) atTop (𝓝 (indicator (closure E) (fun x => 1) x))
x : α
⊢ indicator (closure E) (fun x => 1) x = ENNReal.toNNReal (indicator (closure E) (fun x => 1) x)
refine' (congr_fun (comp_indicator_const 1 ENNReal.toNNReal zero_toNNReal) x).symm