csInf_image — Mathlib

English

Under dual conditions to csSup_image, the infimum of the image is the infimum over the set.

Русский

При симметричных условиях инфиму́м образа равен инфиму́му по множеству.

LaTeX

$$$\inf (f''s) = \inf\{f(a) : a \in s\}.$$$

Lean4

theorem csInf_image [Nonempty β] {s : Set β} (hs : s.Nonempty) {f : β → α} (hf : BddBelow (Set.range fun i : s ↦ f i))
    (hf' : ⨅ i : s, f i ≤ sInf ∅) : sInf (f '' s) = ⨅ a ∈ s, f a :=
  csSup_image (α := αᵒᵈ) hs hf hf'

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