mem_range_self

Mathlib.Data.Set.Operations

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

English

For i ∈ ι, f(i) ∈ range f.

Русский

Пусть i ∈ ι; тогда f(i) ∈ range f.

LaTeX

$$$f(i) \\in \\mathrm{range}(f)$$$

Lean4

@[mfld_simps]
theorem mem_range_self (i : ι) : f i ∈ range f :=
  ⟨i, rfl⟩

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

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

Разделы

Аффилиация

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