one_le_of_ne_zero — Mathlib

English

If k ∈ Fin(n) and k ≠ 0, then 1 ≤ k.

Русский

Если k ∈ Fin(n) и k ≠ 0, то 1 ≤ k.

LaTeX

$$$$\forall k:\\mathrm{Fin}(n),\; k\neq 0 \Rightarrow 1\le k.$$$$

Lean4

theorem one_le_of_ne_zero {n : ℕ} [NeZero n] {k : Fin n} (hk : k ≠ 0) : 1 ≤ k :=
  by
  obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (NeZero.ne n)
  cases n with
  | zero => simp only [Fin.isValue, Fin.zero_le]
  | succ n => rwa [Fin.le_iff_val_le_val, Fin.val_one, Nat.one_le_iff_ne_zero, val_ne_zero_iff]

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