find_eq_iff — Mathlib

English

The statement find(h) = m is equivalent to p(m) and there is no smaller witness.

Русский

Утверждение find(h) = m эквивалентно p(m) и отсутствию меньшего свидетеля.

LaTeX

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

Lean4

theorem find_eq_iff : PNat.find h = m ↔ p m ∧ ∀ n < m, ¬p n :=
  by
  constructor
  · rintro rfl
    exact ⟨PNat.find_spec h, fun _ => PNat.find_min h⟩
  · rintro ⟨hm, hlt⟩
    exact le_antisymm (PNat.find_min' h hm) (not_lt.1 <| imp_not_comm.1 (hlt _) <| PNat.find_spec h)

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