lt_find_iff — Mathlib

English

The lt_find_iff lemma expresses equivalence between lt relations after offsetting by 1 and the predicate p.

Русский

Лемма lt_find_iff выражает эквивалентность между отношением меньшего и предикатом p после прибавления единицы.

LaTeX

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

Lean4

@[simp]
theorem lt_find_iff (n : ℕ+) : n < PNat.find h ↔ ∀ m ≤ n, ¬p m := by
  simp only [← add_one_le_iff, le_find_iff, add_le_add_iff_right]

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