mem_span_range_self

Mathlib.RingTheory.Ideal.Span

URI: https://scilib.ai/kg/mathlib#Ideal.mem_span_range_self

English

For a function f, the value f(x) lies in the span of the range of f.

Русский

Значение f(x) принадлежит порождению диапазона функции f.

LaTeX

$$$f(x) \\in \\operatorname{span}(\\operatorname{range}(f))$$$

Lean4

theorem mem_span_range_self {β : Type*} {f : β → α} {x : β} : f x ∈ span (range f) :=
  subset_span (mem_range_self x)

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

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

Разделы

Аффилиация

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