α : Type u_1
β : Type u_2
γ : Type ?u.468150
δ : Type ?u.468153
inst✝⁵ : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : ↑f' ≤ᵐ[μ] ↑f
hg : ↑f' ≤ᵐ[μ] ↑g
⊢ ↑f' ≤ᵐ[μ] ↑(f ⊓ g)
α : Type u_1
β : Type u_2
γ : Type ?u.468150
δ : Type ?u.468153
inst✝⁵ : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : f' ≤ f
hg : f' ≤ g
⊢ f' ≤ f ⊓ g
rw [← coeFn_le] at hf hg⊢
case h
α : Type u_1
β : Type u_2
γ : Type ?u.468150
δ : Type ?u.468153
inst✝⁵ : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : ↑f' ≤ᵐ[μ] ↑f
hg : ↑f' ≤ᵐ[μ] ↑g
a✝ : α
haf : ↑f' a✝ ≤ ↑f a✝
hag : ↑f' a✝ ≤ ↑g a✝
ha_inf : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑f' a✝ ≤ ↑(f ⊓ g) a✝
α : Type u_1
β : Type u_2
γ : Type ?u.468150
δ : Type ?u.468153
inst✝⁵ : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : ↑f' ≤ᵐ[μ] ↑f
hg : ↑f' ≤ᵐ[μ] ↑g
⊢ ↑f' ≤ᵐ[μ] ↑(f ⊓ g)
filter_upwards [hf, hg, coeFn_inf f g] with _ haf hag ha_inf
case h
α : Type u_1
β : Type u_2
γ : Type ?u.468150
δ : Type ?u.468153
inst✝⁵ : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : ↑f' ≤ᵐ[μ] ↑f
hg : ↑f' ≤ᵐ[μ] ↑g
a✝ : α
haf : ↑f' a✝ ≤ ↑f a✝
hag : ↑f' a✝ ≤ ↑g a✝
ha_inf : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑f' a✝ ≤ ↑f a✝ ⊓ ↑g a✝
case h
α : Type u_1
β : Type u_2
γ : Type ?u.468150
δ : Type ?u.468153
inst✝⁵ : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : ↑f' ≤ᵐ[μ] ↑f
hg : ↑f' ≤ᵐ[μ] ↑g
a✝ : α
haf : ↑f' a✝ ≤ ↑f a✝
hag : ↑f' a✝ ≤ ↑g a✝
ha_inf : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑f' a✝ ≤ ↑(f ⊓ g) a✝
rw [ha_inf]
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.468150
δ : Type ?u.468153
inst✝⁵ : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f' f g : α →ₘ[μ] β
hf : ↑f' ≤ᵐ[μ] ↑f
hg : ↑f' ≤ᵐ[μ] ↑g
a✝ : α
haf : ↑f' a✝ ≤ ↑f a✝
hag : ↑f' a✝ ≤ ↑g a✝
ha_inf : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑f' a✝ ≤ ↑f a✝ ⊓ ↑g a✝
exact le_inf haf hag