mem_finRange

Mathlib.Data.List.FinRange

URI: https://scilib.ai/kg/mathlib#List.mem_finRange

← MathLib Explorer

English

Every element a of Fin(n) belongs to finRange(n).

Русский

Каждый элемент a из Fin(n) принадлежит finRange(n).

LaTeX

$$$\forall {n:\mathbb{N}}\ (a:Fin\,n), a \in finRange n$$$

Lean4

@[simp]
theorem mem_finRange {n : ℕ} (a : Fin n) : a ∈ finRange n :=
  by
  rw [finRange_eq_pmap_range]
  exact
    mem_pmap.2
      ⟨a.1, mem_range.2 a.2, by
        cases a
        rfl⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru