map_finset_max' — Mathlib

English

If f is monotone, then f(extremum of a finite nonempty set) equals the extremum of the image, i.e., f(max S) = max (f[S]).

Русский

Если f монотонна, то максимум множества сохраняется под отображением: f(max S) = max f[S].

LaTeX

$$$f(\\max' S) = \\max'(\\mathrm{image}(f, S))$ (assuming S nonempty).$$

Lean4

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

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