α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1507495
G : Type ?u.1507498
𝕜 : Type ?u.1507501
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
inst✝ : IsFiniteMeasure μ
hT : DominatedFinMeasAdditive μ T C
x : E
this : (fun x_1 => x) = indicator Set.univ fun x_1 => x
⊢ (setToFun μ T hT fun x_1 => x) = ↑(T Set.univ) x
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1507495
G : Type ?u.1507498
𝕜 : Type ?u.1507501
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
inst✝ : IsFiniteMeasure μ
hT : DominatedFinMeasAdditive μ T C
x : E
⊢ (setToFun μ T hT fun x_1 => x) = ↑(T Set.univ) x
have : (fun _ : α => x) = Set.indicator univ fun _ => x := (indicator_univ _).symm
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1507495
G : Type ?u.1507498
𝕜 : Type ?u.1507501
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
inst✝ : IsFiniteMeasure μ
hT : DominatedFinMeasAdditive μ T C
x : E
this : (fun x_1 => x) = indicator Set.univ fun x_1 => x
⊢ setToFun μ T hT (indicator Set.univ fun x_1 => x) = ↑(T Set.univ) x
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1507495
G : Type ?u.1507498
𝕜 : Type ?u.1507501
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
inst✝ : IsFiniteMeasure μ
hT : DominatedFinMeasAdditive μ T C
x : E
this : (fun x_1 => x) = indicator Set.univ fun x_1 => x
⊢ (setToFun μ T hT fun x_1 => x) = ↑(T Set.univ) x
rw [this]
no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1507495
G : Type ?u.1507498
𝕜 : Type ?u.1507501
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
inst✝ : IsFiniteMeasure μ
hT : DominatedFinMeasAdditive μ T C
x : E
this : (fun x_1 => x) = indicator Set.univ fun x_1 => x
⊢ setToFun μ T hT (indicator Set.univ fun x_1 => x) = ↑(T Set.univ) x
exact setToFun_indicator_const hT MeasurableSet.univ (measure_ne_top _ _) x