find_lt_iff — Mathlib

English

Nat.find(h) < n if and only if there exists m < n with p(m).

Русский

Nat.find(h) < n тогда и только тогда, когда существует m < n с p(m).

LaTeX

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

Lean4

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

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