English
A dual version: the infimum of the image equals the infimum over the domain under appropriate bounds.
Русский
Двойственная версия: инфиму́м образа равен инфиму́му по области определения при соответствующих ограничениях.
LaTeX
$$$\inf (f''s) = \inf\{f(a) : a \in s\}.$$$
Lean4
theorem ciInf_image {α ι ι' : Type*} [ConditionallyCompleteLattice α] [Nonempty ι] [Nonempty ι'] {s : Set ι}
(hs : s.Nonempty) {f : ι → ι'} {g : ι' → α} (hf : BddBelow (Set.range fun i : s ↦ g (f i)))
(hg' : ⨅ i : s, g (f i) ≤ sInf ∅) : ⨅ i ∈ (f '' s), g i = ⨅ x ∈ s, g (f x) :=
ciSup_image (α := αᵒᵈ) hs hf hg'