find_lt_iff — Mathlib

English

For predicates p, the statement find h is less than n iff there exists m < n with p(m).

Русский

Относительно предиката p, найдённое значение find h меньше n тогда и только тогда, когда существует m < n с p(m).

LaTeX

$$$ \\mathrm{PNat.find}(h) < n \\iff \\exists m < n, p(m) $$$

Lean4

@[simp]
theorem find_lt_iff (n : ℕ+) : PNat.find h < n ↔ ∃ m < n, p m :=
  ⟨fun h2 => ⟨PNat.find h, h2, PNat.find_spec h⟩, fun ⟨_, hmn, hm⟩ => (PNat.find_min' h hm).trans_lt hmn⟩

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