mem_ofFn'

Mathlib.Data.List.OfFn

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

English

For any a and f, a belongs to the list of f if and only if a belongs to the range of f.

Русский

Элемент a принадлежит списку,List.ofFn f тогда и только тогда, когда a ∈ диапазон f.

LaTeX

$$$ a \\in \\operatorname{List.ofFn} f \\quad\\iff\\quad a \\in \\mathrm{Set.range}(f) $$$

Lean4

theorem mem_ofFn' {n} (f : Fin n → α) (a : α) : a ∈ ofFn f ↔ a ∈ Set.range f := by grind

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

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

Разделы

Аффилиация

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