max'_image — Mathlib

English

In the dual order, the minimum corresponds to the maximum, expressed via image under toDual.

Русский

В двойственном порядке минимум соответствует максимуму, выраженное через образ под toDual.

LaTeX

$$$\\mathrm{toDual}(\\min' S) = \\max'(\\mathrm{image}(\\mathrm{toDual}, S)).$$$

Lean4

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

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