isMin_of_apply — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isMin_of_apply (hf : StrictMono f) (ha : IsMin (f a)) : IsMin a :=
  of_not_not fun h ↦
    let ⟨_, hb⟩ := not_isMin_iff.1 h
    (hf hb).not_isMin ha

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