findGreatest_mono_right — Mathlib

English

If ∀ n, P n → Q n, then for any n, findGreatest P n ≤ findGreatest Q n.

Русский

Если для всех n выполняется P n → Q n, то findGreatest P n ≤ findGreatest Q n.

LaTeX

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

Lean4

theorem findGreatest_mono_right (P : ℕ → Prop) [DecidablePred P] {m n} (hmn : m ≤ n) :
    Nat.findGreatest P m ≤ Nat.findGreatest P n := by
  induction hmn with
  | refl => simp
  | step hmk ih =>
    rw [findGreatest_succ]
    split_ifs
    · exact le_trans ih <| le_trans (findGreatest_le _) (le_succ _)
    · exact ih

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