subtypeDomain_eq_zero_iff'

Mathlib.Data.Finsupp.Basic

URI: https://scilib.ai/kg/mathlib#Finsupp.subtypeDomain_eq_zero_iff'

English

The subtypeDomain is zero iff all values on p are zero.

Русский

Подтип-домен равен нулю тогда и только тогда, когда все значения на p равны нулю.

LaTeX

$$$$ f.subtypeDomain p = 0 \\iff \\forall x, p x \\to f x = 0. $$$$

Lean4

theorem subtypeDomain_eq_zero_iff' {f : α →₀ M} : f.subtypeDomain p = 0 ↔ ∀ x, p x → f x = 0 :=
  subtypeDomain_eq_iff_forall (g := 0)

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

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

Разделы

Аффилиация

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