range_list_get

Mathlib.Data.Set.List

URI: https://scilib.ai/kg/mathlib#Set.range_list_get

English

For a list l, the range of l.get equals the set of all elements of l.

Русский

Для списка l множество значений функции l.get совпадает с множеством элементов l.

LaTeX

$$$\\text{range}(l. get) = \\{x \\mid x \\in l\\}$$$

Lean4

@[simp]
theorem range_list_get : range l.get = {x | x ∈ l} := by
  ext x
  rw [mem_setOf_eq, mem_iff_get, mem_range]

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

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

Разделы

Аффилиация

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