val_pos_iff — Mathlib

English

Let n be a positive integer. For every a in Fin(n), the underlying natural number a.val is positive if and only if a is the positive element in Fin(n); equivalently, 0 < a.val iff 0 < a.

Русский

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

LaTeX

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

Lean4

@[simp, norm_cast]
theorem val_pos_iff [NeZero n] {a : Fin n} : 0 < a.val ↔ 0 < a := by rw [← val_fin_lt, val_zero]

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