findGreatest_mono_left — Mathlib

English

If ∀ n, P n → Q n and m ≤ n, then findGreatest P m ≤ findGreatest Q n.

Русский

Если ∀ n, P n → Q n и m ≤ n, то findGreatest P m ≤ findGreatest Q n.

LaTeX

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

Lean4

theorem findGreatest_mono_left [DecidablePred Q] (hPQ : ∀ n, P n → Q n) (n : ℕ) :
    Nat.findGreatest P n ≤ Nat.findGreatest Q n := by
  induction n with
  | zero => rfl
  | succ n hn =>
    by_cases h : P (n + 1)
    · rw [findGreatest_eq h, findGreatest_eq (hPQ _ h)]
    · rw [findGreatest_of_not h]
      exact le_trans hn (Nat.findGreatest_mono_right _ <| le_succ _)

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