isMax_of_apply — Mathlib

English

If f is strictly antitone and f(a) is the minimum, then a is the maximum.

Русский

Если f строго антимонотонна и f(a) — минимум, то a — максимум.

LaTeX

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

Lean4

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

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