compl_mulSupport

Mathlib.Algebra.Notation.Support

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

English

(mulSupport f)^c = {x | f(x) = 1}.

Русский

Дополнение mulSupport f равно множеству {x | f(x) = 1}.

LaTeX

$$$ (\\mathrm{mulSupport} f)^c = \\{ x \\mid f x = 1 \\} $$$

Lean4

@[to_additive]
theorem compl_mulSupport : (mulSupport f)ᶜ = {x | f x = 1} :=
  ext fun _ ↦ notMem_mulSupport

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

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

Разделы

Аффилиация

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