English
Let f be monotone from a preorder α to a ConditionallyCompleteLattice β. Then for every nonempty set s ⊆ α and every B in the lower bounds of s, f(B) is below the infimum of the image of s under f.
Русский
Пусть f: α → β монотонна, где α — предобраз, β — частично полноупорядоченная решётка. Тогда для любого непустого множества s ⊆ α и любого B ∈ нижних границ s выполняется f(B) ≤ inf { f(x) : x ∈ s }.
LaTeX
$$$\forall f:\alpha\to\beta,\;\text{Monotone }f\;\Rightarrow\; \forall s:\ Set\ \alpha,\ s.Nonempty \Rightarrow \forall B\in lowerBounds(s),\; f(B) \le sInf (f '' s)$$$
Lean4
theorem le_csInf_image {s : Set α} (hs : s.Nonempty) {B : α} (hB : B ∈ lowerBounds s) : f B ≤ sInf (f '' s) :=
by
let f' : αᵒᵈ → βᵒᵈ := f
exact csSup_image_le (α := αᵒᵈ) (β := βᵒᵈ) (show Monotone f' from fun x y hxy => h_mono hxy) hs hB
