mulIndicator_empty'

Mathlib.Algebra.Notation.Indicator

URI: https://scilib.ai/kg/mathlib#Set.mulIndicator_empty'

English

A convenience alias: mulIndicator of empty set equals 1.

Русский

Удобное обозначение: mulIndicator пустого множества равен 1.

LaTeX

$$$\mathrm{Set.mulIndicator\,empty'}(f) = 1$$$

Lean4

@[to_additive]
theorem mulIndicator_empty' (f : α → M) : mulIndicator (∅ : Set α) f = 1 :=
  mulIndicator_empty f

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

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

Разделы

Аффилиация

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