le_find_iff — Mathlib

English

The lemma le_find_iff provides an equivalence between le relations and existential predicates for p.

Русский

Лемма le_find_iff устанавливает эквивалентность между отношением ≤ и существовательному предикату для p.

LaTeX

$$$ \\text{(equivalence given by } \\text{le_find_iff})$$$

Lean4

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

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