α : Type u_2
β : Type u_1
ι : Type ?u.57259
E : Type ?u.57262
F : Type ?u.57265
𝕜 : Type ?u.57268
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
n : ℕ
x : β
this : Nonempty ↑s
⊢ ↑(approxOn f hf s y₀ h₀ n) x ∈ s
α : Type u_2
β : Type u_1
ι : Type ?u.57259
E : Type ?u.57262
F : Type ?u.57265
𝕜 : Type ?u.57268
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
n : ℕ
x : β
⊢ ↑(approxOn f hf s y₀ h₀ n) x ∈ s
haveI : Nonempty s := ⟨⟨y₀, h₀⟩⟩
α : Type u_2
β : Type u_1
ι : Type ?u.57259
E : Type ?u.57262
F : Type ?u.57265
𝕜 : Type ?u.57268
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
n : ℕ
x : β
this : Nonempty ↑s
⊢ ∀ (n : ℕ), Nat.casesOn n y₀ (Subtype.val ∘ denseSeq ↑s) ∈ s
α : Type u_2
β : Type u_1
ι : Type ?u.57259
E : Type ?u.57262
F : Type ?u.57265
𝕜 : Type ?u.57268
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
n : ℕ
x : β
this : Nonempty ↑s
⊢ ↑(approxOn f hf s y₀ h₀ n) x ∈ s
suffices ∀ n, (Nat.casesOn n y₀ ((↑) ∘ denseSeq s) : α) ∈ s by apply this
case zero
α : Type u_2
β : Type u_1
ι : Type ?u.57259
E : Type ?u.57262
F : Type ?u.57265
𝕜 : Type ?u.57268
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
n : ℕ
x : β
this : Nonempty ↑s
⊢ Nat.casesOn Nat.zero y₀ (Subtype.val ∘ denseSeq ↑s) ∈ s

case succ
α : Type u_2
β : Type u_1
ι : Type ?u.57259
E : Type ?u.57262
F : Type ?u.57265
𝕜 : Type ?u.57268
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
n✝ : ℕ
x : β
this : Nonempty ↑s
n : ℕ
⊢ Nat.casesOn (Nat.succ n) y₀ (Subtype.val ∘ denseSeq ↑s) ∈ s
α : Type u_2
β : Type u_1
ι : Type ?u.57259
E : Type ?u.57262
F : Type ?u.57265
𝕜 : Type ?u.57268
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
n : ℕ
x : β
this : Nonempty ↑s
⊢ ∀ (n : ℕ), Nat.casesOn n y₀ (Subtype.val ∘ denseSeq ↑s) ∈ s
rintro (_ | n)
no goals
case zero
α : Type u_2
β : Type u_1
ι : Type ?u.57259
E : Type ?u.57262
F : Type ?u.57265
𝕜 : Type ?u.57268
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
n : ℕ
x : β
this : Nonempty ↑s
⊢ Nat.casesOn Nat.zero y₀ (Subtype.val ∘ denseSeq ↑s) ∈ s

case succ
α : Type u_2
β : Type u_1
ι : Type ?u.57259
E : Type ?u.57262
F : Type ?u.57265
𝕜 : Type ?u.57268
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
n✝ : ℕ
x : β
this : Nonempty ↑s
n : ℕ
⊢ Nat.casesOn (Nat.succ n) y₀ (Subtype.val ∘ denseSeq ↑s) ∈ s
exacts [h₀, Subtype.mem _]
no goals
α : Type u_2
β : Type u_1
ι : Type ?u.57259
E : Type ?u.57262
F : Type ?u.57265
𝕜 : Type ?u.57268
inst✝⁴ : MeasurableSpace α
inst✝³ : PseudoEMetricSpace α
inst✝² : OpensMeasurableSpace α
inst✝¹ : MeasurableSpace β
f✝ f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
n : ℕ
x : β
this✝ : Nonempty ↑s
this : ∀ (n : ℕ), Nat.casesOn n y₀ (Subtype.val ∘ denseSeq ↑s) ∈ s
⊢ ↑(approxOn f hf s y₀ h₀ n) x ∈ s
apply this