map_finset_min' — Mathlib

English

If f is monotone, then f(min S) = min (image f of S).

Русский

Если f монотонна, то f(min S) = min образа f(S).

LaTeX

$$$f(\\min' S) = \\min'(\\mathrm{image}(f, S))$$$

Lean4

/-- A version of `Finset.min'_image` with LHS and RHS reversed.
Also, this version assumes that `s` is nonempty, not its image. -/
theorem _root_.Monotone.map_finset_min' [LinearOrder β] {f : α → β} (hf : Monotone f) {s : Finset α} (h : s.Nonempty) :
    f (s.min' h) = (s.image f).min' (h.image f) :=
  .symm <| min'_image hf ..

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