α : Type u_1
β : Type u_2
γ : Type ?u.97518
ι : Sort ?u.97521
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
h_mono : Monotone f
s : Set α
c : α
hcs : c ∈ s
h_bdd : BddBelow s
f' : αᵒᵈ → βᵒᵈ := f
⊢ sInf (f '' s) ≤ f c
α : Type u_1
β : Type u_2
γ : Type ?u.97518
ι : Sort ?u.97521
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
h_mono : Monotone f
s : Set α
c : α
hcs : c ∈ s
h_bdd : BddBelow s
⊢ sInf (f '' s) ≤ f c
let f' : αᵒᵈ → βᵒᵈ := f
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.97518
ι : Sort ?u.97521
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
h_mono : Monotone f
s : Set α
c : α
hcs : c ∈ s
h_bdd : BddBelow s
f' : αᵒᵈ → βᵒᵈ := f
⊢ sInf (f '' s) ≤ f c
exact @le_csSup_image αᵒᵈ βᵒᵈ _ _ _
  (show Monotone f' from fun x y hxy => h_mono hxy) _ _ hcs h_bdd