mulIndicator_univ

Mathlib.Algebra.Notation.Indicator

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

English

The indicator of the universal set with a function equals the function itself.

Русский

Индикатор универсума с функцией равен самой функции.

LaTeX

$$$\mathrm{Set.univ}.\mathrm{mulIndicator}(f) = f$$$

Lean4

@[to_additive (attr := simp)]
theorem mulIndicator_univ (f : α → M) : mulIndicator (univ : Set α) f = f :=
  mulIndicator_eq_self.2 <| subset_univ _

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

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

Разделы

Аффилиация

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