subset_mulTSupport

Mathlib.Topology.Algebra.Support

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

English

The multiplicative support is contained in its topological support: mulSupport f ⊆ mulTSupport f.

Русский

Поддержка умножения содержится в топологической поддержке: mulSupport(f) ⊆ mulTSupport(f).

LaTeX

$$$\operatorname{mulSupport}(f) \subseteq \operatorname{mulTSupport}(f)$$$

Lean4

@[to_additive]
theorem subset_mulTSupport (f : X → α) : mulSupport f ⊆ mulTSupport f :=
  subset_closure

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

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

Разделы

Аффилиация

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