pos_iff_ne_zero' — Mathlib

English

Let n be a positive integer. For every a in Fin(n), the condition 0 < a is equivalent to a ≠ 0; i.e., positivity in Fin coincides with being nonzero.

Русский

Пусть n — положительное число. Для любого a ∈ Fin(n) 0 < a эквивалентно a ≠ 0; то есть положительность в Fin совпадает с не нулём.

LaTeX

$$$$\forall a:\\mathrm{Fin}(n),\; 0 < a \iff a \neq 0.$$$$

Lean4

/-- The `Fin.pos_iff_ne_zero` in `Lean` only applies in `Fin (n+1)`.
This one instead uses a `NeZero n` typeclass hypothesis.
-/
theorem pos_iff_ne_zero' [NeZero n] (a : Fin n) : 0 < a ↔ a ≠ 0 := by
  rw [← val_pos_iff, Nat.pos_iff_ne_zero, val_ne_zero_iff]

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