le_zero_iff' — Mathlib

English

For n with NeZero, for k ∈ Fin n, k ≤ 0 iff k = 0.

Русский

Для n с NeZero, для k ∈ Fin n: k ≤ 0 эквивалентно k = 0.

LaTeX

$$$\\forall n,\\ [\\mathrm{NeZero}\\ n] \\Rightarrow \\forall k \\in \\mathrm{Fin}(n),\\; k \\le 0 \\leftrightarrow k = 0$$$

Lean4

/-- The `Fin.le_zero_iff` in `Lean` only applies in `Fin (n+1)`.
This one instead uses a `NeZero n` typeclass hypothesis.
-/
@[simp]
theorem le_zero_iff' {n : ℕ} [NeZero n] {k : Fin n} : k ≤ 0 ↔ k = 0 :=
  ⟨fun h => Fin.ext <| by rw [Nat.eq_zero_of_le_zero h]; rfl, by rintro rfl; exact Nat.le_refl _⟩
    -- TODO: Move to Batteries

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