findGreatest_pos — Mathlib

English

For any k, 0 < findGreatest P k iff there exists a positive n with 0 < n ≤ k and P n.

Русский

Для любого k выполняется: 0 < findGreatest P k тогда и только тогда, существует положительный n с 0 < n ≤ k и P n.

LaTeX

$$$0 < \operatorname{findGreatest} P k \;\iff\; \exists n\, (0 < n \land n \le k \land P n).$$$

Lean4

@[simp]
theorem findGreatest_pos : 0 < Nat.findGreatest P k ↔ ∃ n, 0 < n ∧ n ≤ k ∧ P n := by
  rw [Nat.pos_iff_ne_zero, Ne, findGreatest_eq_zero_iff]; push_neg; rfl

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