get_finRange — Mathlib

English

Let n ∈ ℕ and i ∈ ℕ with i < n. The i-th element of finRange n is the canonical element ⟨i, i < n⟩ of Fin n; equivalently, (finRange n).get ⟨i, h⟩ = ⟨i, h'⟩ for some h' : i < n.

Русский

Пусть n ∈ ℕ и i ∈ ℕ с i < n. i-й элемент списка finRange n есть канонический элемент ⟨i, i < n⟩ из Fin n; эквивалентно, (finRange n).get ⟨i, h⟩ = ⟨i, h'⟩ для некоторого h' : i < n.

LaTeX

$$$$ (finRange\\,n).\\mathrm{get}\\langle i,h\\rangle = \\langle i,h'\\rangle \\quad \\text{for some } h' : i < n. $$$$

Lean4

theorem get_finRange {n : ℕ} {i : ℕ} (h) : (finRange n).get ⟨i, h⟩ = ⟨i, length_finRange (n := n) ▸ h⟩ := by simp

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