image_eq_one_of_notMem_mulTSupport

Mathlib.Topology.Algebra.Support

URI: https://scilib.ai/kg/mathlib#image_eq_one_of_notMem_mulTSupport

← MathLib Explorer

English

If x is not in mulTSupport f, then f(x) = 1.

Русский

Если x не принадлежит mulTSupport f, то f(x) = 1.

LaTeX

$$$\,x \notin \operatorname{mulTSupport}(f) \Rightarrow f(x) = 1$$$

Lean4

@[to_additive]
theorem image_eq_one_of_notMem_mulTSupport {f : X → α} {x : X} (hx : x ∉ mulTSupport f) : f x = 1 :=
  mulSupport_subset_iff'.mp (subset_mulTSupport f) x hx

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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