find_mono — Mathlib

English

A weaker monotonicity: if q implies p everywhere, then Nat.find(h_p) ≤ Nat.find(h_q).

Русский

Ослабленная монотонность: если $q$ везде подразумевает $p$, то Nat.find(h_p) ≤ Nat.find(h_q).

LaTeX

$$$\\mathrm{Nat.find}(hp) \\le \\mathrm{Nat.find}(hq).$$$

Lean4

/-- A weak version of `Nat.find_mono_of_le`, requiring `q` implies `p` everywhere.
-/
theorem find_mono [DecidablePred q] (h : ∀ n, q n → p n) {hp : ∃ n, p n} {hq : ∃ n, q n} : Nat.find hp ≤ Nat.find hq :=
  let ⟨_, hq⟩ := hq;
  find_mono_of_le hq fun _ _ ↦ h _

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