α : Type u_1
β : Type u_2
γ : Type ?u.98153
ι : Sort ?u.98156
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
h_mono : Monotone f
s : Set α
hs : Set.Nonempty s
B : α
hB : B ∈ lowerBounds s
f' : αᵒᵈ → βᵒᵈ := f
⊢ f B ≤ sInf (f '' s)
α : Type u_1
β : Type u_2
γ : Type ?u.98153
ι : Sort ?u.98156
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
h_mono : Monotone f
s : Set α
hs : Set.Nonempty s
B : α
hB : B ∈ lowerBounds s
⊢ f B ≤ sInf (f '' s)
let f' : αᵒᵈ → βᵒᵈ := f
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.98153
ι : Sort ?u.98156
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
h_mono : Monotone f
s : Set α
hs : Set.Nonempty s
B : α
hB : B ∈ lowerBounds s
f' : αᵒᵈ → βᵒᵈ := f
⊢ f B ≤ sInf (f '' s)
exact @csSup_image_le αᵒᵈ βᵒᵈ _ _ _
  (show Monotone f' from fun x y hxy => h_mono hxy) _ hs _ hB