ciInf_image — Mathlib

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'

Похожие утверждения