toFinset_range

Mathlib.Order.Interval.Finset.Nat

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

English

List.range a, when converted to a Finset, equals Finset.range a.

Русский

List.range a, преобразованный в Finset, равен Finset.range a.

LaTeX

$$$(List.range\\ a).toFinset = Finset.range\\ a$$$

Lean4

theorem toFinset_range (a : ℕ) : (List.range a).toFinset = Finset.range a :=
  by
  ext x
  rw [List.mem_toFinset, List.mem_range, Finset.mem_range]

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

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

Разделы

Аффилиация

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