toFinset_range'_1_1

Mathlib.Order.Interval.Finset.Nat

URI: https://scilib.ai/kg/mathlib#List.toFinset_range'_1_1

← MathLib Explorer

English

The Finset derived from List.range' 1 a is the interval Icc 1 a.

Русский

Из List.range' 1 a получается интервал Icc 1 a.

LaTeX

$$$ (List.range' 1 \\\\text{a}).toFinset = Icc\\ 1\\ a $$$

Lean4

theorem toFinset_range'_1_1 (a : ℕ) : (List.range' 1 a).toFinset = Icc 1 a :=
  by
  ext x
  rw [List.mem_toFinset, List.mem_range'_1, add_comm, Nat.lt_succ_iff, Finset.mem_Icc]

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

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

Разделы

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

Аффилиация

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