notMem_mulSupport

Mathlib.Algebra.Notation.Support

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

English

x ∉ mulSupport f if and only if f(x) = 1.

Русский

x не принадлежит mulSupport f тогда и только тогда, когда f(x) = 1.

LaTeX

$$$ x \\notin \\mathrm{mulSupport}(f) \\iff f(x) = 1 $$$

Lean4

@[to_additive]
theorem notMem_mulSupport : x ∉ mulSupport f ↔ f x = 1 :=
  not_not

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

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

Разделы

Аффилиация

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