mulSupport_const

Mathlib.Algebra.Notation.Support

URI: https://scilib.ai/kg/mathlib#Function.mulSupport_const

English

If c ≠ 1, then every point lies in the support of the constant function c.

Русский

Если c ≠ 1, то каждая точка принадлежит опоре константной функции c.

LaTeX

$$$ c \neq 1 \implies \operatorname{mulSupport}(\lambda \_ : \iota \mapsto c) = \operatorname{univ} $$$

Lean4

@[to_additive]
theorem mulSupport_const {c : M} (hc : c ≠ 1) : (mulSupport fun _ : ι ↦ c) = Set.univ := by ext x; simp [hc]

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

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

Разделы

Аффилиация

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