find_mono — Mathlib

English

Theorem find_mono states that if q(n) implies p(n) for all n, then the minimal witnesses respect the same order: find hp ≤ find hq.

Русский

Теорема find_mono говорит, что если q(n) ⇒ p(n) для всех n, то минимальные свидетели сохраняют порядок: find hp ≤ find hq.

LaTeX

$$$ \\forall n,\\ q(n) \\Rightarrow p(n) \\;\\Rightarrow\\; \\mathrm{PNat.find}(hp) \\le \\mathrm{PNat.find}(hq) $$$

Lean4

theorem find_mono (h : ∀ n, q n → p n) {hp : ∃ n, p n} {hq : ∃ n, q n} : PNat.find hp ≤ PNat.find hq :=
  PNat.find_min' _ (h _ (PNat.find_spec hq))

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