α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1503019
G : Type ?u.1503022
𝕜 : Type ?u.1503025
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
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : E
⊢ setToFun μ T hT ↑↑(indicatorConstLp 1 hs hμs x) = ↑(T s) x
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1503019
G : Type ?u.1503022
𝕜 : Type ?u.1503025
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
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : E
⊢ setToFun μ T hT (indicator s fun x_1 => x) = ↑(T s) x
rw [setToFun_congr_ae hT (@indicatorConstLp_coeFn _ _ _ 1 _ _ _ hs hμs x).symm]
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1503019
G : Type ?u.1503022
𝕜 : Type ?u.1503025
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
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : E
⊢ ↑(L1.setToL1 hT) (indicatorConstLp 1 hs hμs x) = ↑(T s) x
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1503019
G : Type ?u.1503022
𝕜 : Type ?u.1503025
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
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : E
⊢ setToFun μ T hT ↑↑(indicatorConstLp 1 hs hμs x) = ↑(T s) x
rw [L1.setToFun_eq_setToL1 hT]
no goals
α : Type u_1
E : Type u_2
F : Type u_3
F' : Type ?u.1503019
G : Type ?u.1503022
𝕜 : Type ?u.1503025
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
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : ↑↑μ s ≠ ⊤
x : E
⊢ ↑(L1.setToL1 hT) (indicatorConstLp 1 hs hμs x) = ↑(T s) x
exact L1.setToL1_indicatorConstLp hT hs hμs x