α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.152425
inst✝¹ : CompleteLattice α
f g✝ : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ ↑g (⨅ (s : Set β) (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), u b) ≤
    ⨅ (s : Set β) (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), ↑g (u b)
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.152425
inst✝¹ : CompleteLattice α
f g✝ : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ ↑g (blimsup u f p) ≤ blimsup (↑g ∘ u) f p
simp only [blimsup_eq_iInf_biSup, Function.comp]
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.152425
inst✝¹ : CompleteLattice α
f g✝ : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ (⨅ (i : Set β) (_ : i ∈ f), ↑g (⨆ (b : β) (_ : p b ∧ b ∈ i), u b)) ≤
    ⨅ (s : Set β) (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), ↑g (u b)
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.152425
inst✝¹ : CompleteLattice α
f g✝ : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ ↑g (⨅ (s : Set β) (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), u b) ≤
    ⨅ (s : Set β) (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), ↑g (u b)
refine' ((OrderHomClass.mono g).map_iInf₂_le _).trans _
no goals
α : Type u_2
β : Type u_3
γ : Type u_1
ι : Type ?u.152425
inst✝¹ : CompleteLattice α
f g✝ : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ (⨅ (i : Set β) (_ : i ∈ f), ↑g (⨆ (b : β) (_ : p b ∧ b ∈ i), u b)) ≤
    ⨅ (s : Set β) (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), ↑g (u b)
simp only [_root_.map_iSup, le_refl]