toFinset_range'_1

Mathlib.Order.Interval.Finset.Nat

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

← MathLib Explorer

English

The Finset obtained from List.range' a b equals the Finset Ico a (a+b).

Русский

Финсет, полученный из List.range' a b, равен Finset Ico a (a+b).

LaTeX

$$$ (List.range' a b).toFinset = Ico\\ a\\ (a + b) $$$

Lean4

theorem toFinset_range'_1 (a b : ℕ) : (List.range' a b).toFinset = Ico a (a + b) :=
  by
  ext x
  rw [List.mem_toFinset, List.mem_range'_1, Finset.mem_Ico]

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

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

Разделы

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

Аффилиация

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