min'_image — Mathlib

English

For a monotone function f, the minimum of the image equals the image of the minimum of the preimage.

Русский

Для монотонной функции f минимум образа равен образу минимума предобраза.

LaTeX

$$$(\\operatorname{image} f)\\,\\min' h = f(\\min' h.ob) $$$

Lean4

/-- To rewrite from right to left, use `Monotone.map_finset_min'`. -/
@[simp]
theorem min'_image [LinearOrder β] {f : α → β} (hf : Monotone f) (s : Finset α) (h : (s.image f).Nonempty) :
    (s.image f).min' h = f (s.min' h.of_image) :=
  by
  simp only [min', inf'_image]
  exact .symm <| comp_inf'_eq_inf'_comp _ _ fun _ _ ↦ hf.map_min

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