mulSupport_subset_iff'

Mathlib.Algebra.Notation.Support

URI: https://scilib.ai/kg/mathlib#Function.mulSupport_subset_iff'

English

mulSupport f ⊆ s iff for all x ∉ s, f(x) = 1.

Русский

mulSupport f ⊆ s эквивалентно тому, что для всех x ∉ s выполняется f(x) = 1.

LaTeX

$$$ \\mathrm{mulSupport}(f) \\subseteq s \\iff \\forall x, x \\notin s \\rightarrow f(x) = 1 $$$

Lean4

@[to_additive]
theorem mulSupport_subset_iff' : mulSupport f ⊆ s ↔ ∀ x ∉ s, f x = 1 :=
  forall_congr' fun _ ↦ not_imp_comm

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

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

Разделы

Аффилиация

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