find_eq_iff — Mathlib

English

Nat.find(h) equals m exactly when p(m) holds and no smaller n satisfies p.

Русский

Nat.find(h) равно m тогда и только тогда, когда p(m) выполнено и для всех n < m ¬p(n).

LaTeX

$$$\\mathrm{Nat.find}(h) = m \\iff p(m) \\land \\forall n < m, \\lnot p(n).$$$

Lean4

theorem find_eq_iff (h : ∃ n : ℕ, p n) : Nat.find h = m ↔ p m ∧ ∀ n < m, ¬p n :=
  by
  constructor
  · grind [Nat.find_min]
  · rintro ⟨hm, hlt⟩
    have := Nat.find_min' h hm
    grind

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