α : Type u_1
β : Type ?u.2310097
ι : Type ?u.2310100
E : Type ?u.2310103
F : Type ?u.2310106
𝕜 : Type ?u.2310109
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
⊢ 0 ≤ᵐ[μ] ↑↑↑f ↔ ↑↑↑0 ≤ᵐ[μ] ↑↑↑f
α : Type u_1
β : Type ?u.2310097
ι : Type ?u.2310100
E : Type ?u.2310103
F : Type ?u.2310106
𝕜 : Type ?u.2310109
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
⊢ 0 ≤ᵐ[μ] ↑↑↑f ↔ 0 ≤ f
rw [← Lp.simpleFunc.coeFn_le]
α : Type u_1
β : Type ?u.2310097
ι : Type ?u.2310100
E : Type ?u.2310103
F : Type ?u.2310106
𝕜 : Type ?u.2310109
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
h0 : ↑↑↑0 =ᵐ[μ] 0
⊢ 0 ≤ᵐ[μ] ↑↑↑f ↔ ↑↑↑0 ≤ᵐ[μ] ↑↑↑f
α : Type u_1
β : Type ?u.2310097
ι : Type ?u.2310100
E : Type ?u.2310103
F : Type ?u.2310106
𝕜 : Type ?u.2310109
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
⊢ 0 ≤ᵐ[μ] ↑↑↑f ↔ ↑↑↑0 ≤ᵐ[μ] ↑↑↑f
have h0 : (0 : Lp.simpleFunc G p μ) =ᵐ[μ] (0 : α → G) := Lp.simpleFunc.coeFn_zero p μ G
case h
α : Type u_1
β : Type ?u.2310097
ι : Type ?u.2310100
E : Type ?u.2310103
F : Type ?u.2310106
𝕜 : Type ?u.2310109
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
h0 : ↑↑↑0 =ᵐ[μ] 0
h : 0 ≤ᵐ[μ] ↑↑↑f
a✝¹ : α
a✝ : OfNat.ofNat 0 a✝¹ ≤ ↑↑↑f a✝¹
h2 : ↑↑↑0 a✝¹ = OfNat.ofNat 0 a✝¹
⊢ ↑↑↑0 a✝¹ ≤ ↑↑↑f a✝¹

case h
α : Type u_1
β : Type ?u.2310097
ι : Type ?u.2310100
E : Type ?u.2310103
F : Type ?u.2310106
𝕜 : Type ?u.2310109
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
h0 : ↑↑↑0 =ᵐ[μ] 0
h : ↑↑↑0 ≤ᵐ[μ] ↑↑↑f
a✝¹ : α
a✝ : ↑↑↑0 a✝¹ ≤ ↑↑↑f a✝¹
h2 : ↑↑↑0 a✝¹ = OfNat.ofNat 0 a✝¹
⊢ OfNat.ofNat 0 a✝¹ ≤ ↑↑↑f a✝¹
α : Type u_1
β : Type ?u.2310097
ι : Type ?u.2310100
E : Type ?u.2310103
F : Type ?u.2310106
𝕜 : Type ?u.2310109
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
h0 : ↑↑↑0 =ᵐ[μ] 0
⊢ 0 ≤ᵐ[μ] ↑↑↑f ↔ ↑↑↑0 ≤ᵐ[μ] ↑↑↑f
constructor <;> intro h <;> filter_upwards [h, h0] with _ _ h2
no goals
case h
α : Type u_1
β : Type ?u.2310097
ι : Type ?u.2310100
E : Type ?u.2310103
F : Type ?u.2310106
𝕜 : Type ?u.2310109
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
h0 : ↑↑↑0 =ᵐ[μ] 0
h : 0 ≤ᵐ[μ] ↑↑↑f
a✝¹ : α
a✝ : OfNat.ofNat 0 a✝¹ ≤ ↑↑↑f a✝¹
h2 : ↑↑↑0 a✝¹ = OfNat.ofNat 0 a✝¹
⊢ ↑↑↑0 a✝¹ ≤ ↑↑↑f a✝¹
rwa [h2]
no goals
case h
α : Type u_1
β : Type ?u.2310097
ι : Type ?u.2310100
E : Type ?u.2310103
F : Type ?u.2310106
𝕜 : Type ?u.2310109
inst✝³ : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
p : ℝ≥0∞
μ : Measure α
G : Type u_2
inst✝ : NormedLatticeAddCommGroup G
f : { x // x ∈ simpleFunc G p μ }
h0 : ↑↑↑0 =ᵐ[μ] 0
h : ↑↑↑0 ≤ᵐ[μ] ↑↑↑f
a✝¹ : α
a✝ : ↑↑↑0 a✝¹ ≤ ↑↑↑f a✝¹
h2 : ↑↑↑0 a✝¹ = OfNat.ofNat 0 a✝¹
⊢ OfNat.ofNat 0 a✝¹ ≤ ↑↑↑f a✝¹
rwa [← h2]