α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1772080
G : Type ?u.1772083
𝕜 : Type ?u.1772086
p : ℝ≥0∞
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
inst✝³ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝² : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
X : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ (x : X), x ∈ s → AEStronglyMeasurable (fs x) μ
h_bound : ∀ (x : X), x ∈ s → ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => fs x a) s
x : X
hx : x ∈ s
⊢ ContinuousWithinAt (fun x => setToFun μ T hT (fs x)) s x
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1772080
G : Type ?u.1772083
𝕜 : Type ?u.1772086
p : ℝ≥0∞
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
inst✝³ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝² : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
X : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ (x : X), x ∈ s → AEStronglyMeasurable (fs x) μ
h_bound : ∀ (x : X), x ∈ s → ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => fs x a) s
⊢ ContinuousOn (fun x => setToFun μ T hT (fs x)) s
intro x hx
case refine'_1
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1772080
G : Type ?u.1772083
𝕜 : Type ?u.1772086
p : ℝ≥0∞
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
inst✝³ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝² : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
X : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ (x : X), x ∈ s → AEStronglyMeasurable (fs x) μ
h_bound : ∀ (x : X), x ∈ s → ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => fs x a) s
x : X
hx : x ∈ s
⊢ ∀ᶠ (x : X) in 𝓝[s] x, AEStronglyMeasurable (fs x) μ

case refine'_2
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1772080
G : Type ?u.1772083
𝕜 : Type ?u.1772086
p : ℝ≥0∞
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
inst✝³ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝² : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
X : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ (x : X), x ∈ s → AEStronglyMeasurable (fs x) μ
h_bound : ∀ (x : X), x ∈ s → ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => fs x a) s
x : X
hx : x ∈ s
⊢ ∀ᶠ (x : X) in 𝓝[s] x, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a

case refine'_3
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1772080
G : Type ?u.1772083
𝕜 : Type ?u.1772086
p : ℝ≥0∞
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
inst✝³ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝² : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
X : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ (x : X), x ∈ s → AEStronglyMeasurable (fs x) μ
h_bound : ∀ (x : X), x ∈ s → ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => fs x a) s
x : X
hx : x ∈ s
⊢ ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x => fs x a) s x
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1772080
G : Type ?u.1772083
𝕜 : Type ?u.1772086
p : ℝ≥0∞
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
inst✝³ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝² : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
X : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ (x : X), x ∈ s → AEStronglyMeasurable (fs x) μ
h_bound : ∀ (x : X), x ∈ s → ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => fs x a) s
x : X
hx : x ∈ s
⊢ ContinuousWithinAt (fun x => setToFun μ T hT (fs x)) s x
refine' continuousWithinAt_setToFun_of_dominated hT _ _ bound_integrable _
no goals
case refine'_1
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1772080
G : Type ?u.1772083
𝕜 : Type ?u.1772086
p : ℝ≥0∞
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
inst✝³ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝² : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
X : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ (x : X), x ∈ s → AEStronglyMeasurable (fs x) μ
h_bound : ∀ (x : X), x ∈ s → ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => fs x a) s
x : X
hx : x ∈ s
⊢ ∀ᶠ (x : X) in 𝓝[s] x, AEStronglyMeasurable (fs x) μ
filter_upwards [self_mem_nhdsWithin] with x hx using hfs_meas x hx
no goals
case refine'_2
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1772080
G : Type ?u.1772083
𝕜 : Type ?u.1772086
p : ℝ≥0∞
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
inst✝³ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝² : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
X : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ (x : X), x ∈ s → AEStronglyMeasurable (fs x) μ
h_bound : ∀ (x : X), x ∈ s → ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => fs x a) s
x : X
hx : x ∈ s
⊢ ∀ᶠ (x : X) in 𝓝[s] x, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
filter_upwards [self_mem_nhdsWithin] with x hx using h_bound x hx
no goals
case refine'_3
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1772080
G : Type ?u.1772083
𝕜 : Type ?u.1772086
p : ℝ≥0∞
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedAddCommGroup F'
inst✝⁴ : NormedSpace ℝ F'
inst✝³ : NormedAddCommGroup G
m : MeasurableSpace α
μ : Measure α
inst✝² : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
f g : α → E
X : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ (x : X), x ∈ s → AEStronglyMeasurable (fs x) μ
h_bound : ∀ (x : X), x ∈ s → ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => fs x a) s
x : X
hx : x ∈ s
⊢ ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x => fs x a) s x
filter_upwards [h_cont] with a ha using ha x hx