α : Type u_2
β : Type u_1
β₂ : Type ?u.78898
γ : Type ?u.78901
ι : Sort ?u.78904
ι' : Sort ?u.78907
κ : ι → Sort ?u.78912
κ' : ι' → Sort ?u.78917
inst✝¹ : CompleteLattice α
f✝ g s✝ t : ι → α
a b : α
inst✝ : CompleteLattice β
s : Set α
f : α → β
hf : Monotone f
⊢ (⨆ (a : α) (_ : a ∈ s), f a) ≤ f (⨆ (a : α) (_ : a ∈ s), a)
α : Type u_2
β : Type u_1
β₂ : Type ?u.78898
γ : Type ?u.78901
ι : Sort ?u.78904
ι' : Sort ?u.78907
κ : ι → Sort ?u.78912
κ' : ι' → Sort ?u.78917
inst✝¹ : CompleteLattice α
f✝ g s✝ t : ι → α
a b : α
inst✝ : CompleteLattice β
s : Set α
f : α → β
hf : Monotone f
⊢ (⨆ (a : α) (_ : a ∈ s), f a) ≤ f (sSup s)
rw [sSup_eq_iSup]
no goals
α : Type u_2
β : Type u_1
β₂ : Type ?u.78898
γ : Type ?u.78901
ι : Sort ?u.78904
ι' : Sort ?u.78907
κ : ι → Sort ?u.78912
κ' : ι' → Sort ?u.78917
inst✝¹ : CompleteLattice α
f✝ g s✝ t : ι → α
a b : α
inst✝ : CompleteLattice β
s : Set α
f : α → β
hf : Monotone f
⊢ (⨆ (a : α) (_ : a ∈ s), f a) ≤ f (⨆ (a : α) (_ : a ∈ s), a)
exact hf.le_map_iSup₂ _