α : Type u_1
β : Type u_2
γ : Type ?u.458131
δ : Type ?u.458134
inst✝⁵ : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : ↑f ≤ᵐ[μ] ↑f'
hg : ↑g ≤ᵐ[μ] ↑f'
⊢ ↑(f ⊔ g) ≤ᵐ[μ] ↑f'
α : Type u_1
β : Type u_2
γ : Type ?u.458131
δ : Type ?u.458134
inst✝⁵ : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : f ≤ f'
hg : g ≤ f'
⊢ f ⊔ g ≤ f'
rw [← coeFn_le] at hf hg⊢
case h
α : Type u_1
β : Type u_2
γ : Type ?u.458131
δ : Type ?u.458134
inst✝⁵ : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : ↑f ≤ᵐ[μ] ↑f'
hg : ↑g ≤ᵐ[μ] ↑f'
a✝ : α
haf : ↑f a✝ ≤ ↑f' a✝
hag : ↑g a✝ ≤ ↑f' a✝
ha_sup : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝
⊢ ↑(f ⊔ g) a✝ ≤ ↑f' a✝
α : Type u_1
β : Type u_2
γ : Type ?u.458131
δ : Type ?u.458134
inst✝⁵ : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : ↑f ≤ᵐ[μ] ↑f'
hg : ↑g ≤ᵐ[μ] ↑f'
⊢ ↑(f ⊔ g) ≤ᵐ[μ] ↑f'
filter_upwards [hf, hg, coeFn_sup f g] with _ haf hag ha_sup
case h
α : Type u_1
β : Type u_2
γ : Type ?u.458131
δ : Type ?u.458134
inst✝⁵ : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : ↑f ≤ᵐ[μ] ↑f'
hg : ↑g ≤ᵐ[μ] ↑f'
a✝ : α
haf : ↑f a✝ ≤ ↑f' a✝
hag : ↑g a✝ ≤ ↑f' a✝
ha_sup : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝
⊢ ↑f a✝ ⊔ ↑g a✝ ≤ ↑f' a✝
case h
α : Type u_1
β : Type u_2
γ : Type ?u.458131
δ : Type ?u.458134
inst✝⁵ : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : ↑f ≤ᵐ[μ] ↑f'
hg : ↑g ≤ᵐ[μ] ↑f'
a✝ : α
haf : ↑f a✝ ≤ ↑f' a✝
hag : ↑g a✝ ≤ ↑f' a✝
ha_sup : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝
⊢ ↑(f ⊔ g) a✝ ≤ ↑f' a✝
rw [ha_sup]
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.458131
δ : Type ?u.458134
inst✝⁵ : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : SemilatticeSup β
inst✝ : ContinuousSup β
f g f' : α →ₘ[μ] β
hf : ↑f ≤ᵐ[μ] ↑f'
hg : ↑g ≤ᵐ[μ] ↑f'
a✝ : α
haf : ↑f a✝ ≤ ↑f' a✝
hag : ↑g a✝ ≤ ↑f' a✝
ha_sup : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝
⊢ ↑f a✝ ⊔ ↑g a✝ ≤ ↑f' a✝
exact sup_le haf hag