mulIndicator_mulSupport

Mathlib.Algebra.Notation.Indicator

URI: https://scilib.ai/kg/mathlib#Set.mulIndicator_mulSupport

Lean4

@[to_additive (attr := simp)]
theorem mulIndicator_mulSupport : mulIndicator (mulSupport f) f = f :=
  mulIndicator_eq_self.2 Subset.rfl

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

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

Разделы

Аффилиация

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