instCanLiftNatValLt — Mathlib

English

For each n, every k < n yields an element ⟨k, hk⟩ in Fin n, and its natural value is k.

Русский

Для каждого n каждый k < n отображается в Fin n как элемент ⟨k, hk⟩, причём его натуральное значение равно k.

LaTeX

$$$\forall n \in \mathbb{N}, \forall k \in \mathbb{N}, (k < n) \Rightarrow \operatorname{val}(\langle k, hk\rangle) = k$$$

Lean4

instance {n : ℕ} : CanLift ℕ (Fin n) Fin.val (· < n) where prf k hk := ⟨⟨k, hk⟩, rfl⟩

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