mulIndicator_empty — Mathlib

English

The indicator of the empty set with a function equals the constant 1 function.

Русский

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

LaTeX

$$$\mathrm{Set.instEmptyCollection.emptyCollection}.\mathrm{mulIndicator} f = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem mulIndicator_empty (f : α → M) : mulIndicator (∅ : Set α) f = fun _ => 1 :=
  mulIndicator_eq_one.2 <| disjoint_empty _

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