isMin_of_apply — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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