findGreatest_eq_zero_iff — Mathlib

English

Let P: N → Prop be a decidable predicate and k ∈ N. Then findGreatest P k equals 0 exactly when no positive n ≤ k satisfies P n.

Русский

Пусть P: ℕ → Prop — разрешимый предикат, и k ∈ ℕ. Тогда findGreatest P k = 0 тогда и только тогда, когда для всех положительных n ≤ k не выполняется P(n).

LaTeX

$$$\mathrm{findGreatest} P k = 0 \;\Longleftrightarrow\; \forall n\, (0 < n \rightarrow n \le k \rightarrow \neg P n).$$$

Lean4

theorem findGreatest_eq_zero_iff : Nat.findGreatest P k = 0 ↔ ∀ ⦃n⦄, 0 < n → n ≤ k → ¬P n := by
  simp [findGreatest_eq_iff]

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