findGreatest_mono — Mathlib

English

For any m,n and predicates P,Q with the condition P n → Q n, the inequality compare of findGreatest holds: findGreatest P m ≤ findGreatest Q n when m ≤ n.

Русский

Для любых m,n и предикатов P,Q с условием P n → Q n, выполняется неравенство: findGreatest P m ≤ findGreatest Q n при m ≤ n.

LaTeX

$$$(\forall n, P n \to Q n) \to (m \le n) \Rightarrow \mathrm{findGreatest} P m \le \mathrm{findGreatest} Q n.$$$

Lean4

theorem findGreatest_mono [DecidablePred Q] (hPQ : ∀ n, P n → Q n) (hmn : m ≤ n) :
    Nat.findGreatest P m ≤ Nat.findGreatest Q n :=
  le_trans (Nat.findGreatest_mono_right _ hmn) (findGreatest_mono_left hPQ _)

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