isMax_of_apply — Mathlib

English

If f is strictly increasing and f(a) is a maximum value, then a is a maximum.

Русский

Если f строго возрастает и f(a) достигает максимума, то a достигает максимума в области определения.

LaTeX

$$$\\forall {\\alpha \\beta} [Preorder \\alpha] [Preorder \\beta] {f : \\alpha \\to \\beta} {a : \\alpha},\\; StrictMono f \\to IsMax (f a) \\to IsMax a$$$

Lean4

theorem isMax_of_apply (hf : StrictMono f) (ha : IsMax (f a)) : IsMax a :=
  of_not_not fun h ↦
    let ⟨_, hb⟩ := not_isMax_iff.1 h
    (hf hb).not_isMax ha

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