mulIndicator_apply — Mathlib

English

For any set s ⊆ α, any function f: α → M, and any a ∈ α, the value (mulIndicator s f) a equals f a if a ∈ s, and equals 1 otherwise.

Русский

Для множества s ⊆ α и функции f: α → M и для любого a ∈ α, значение (mulIndicator s f) a равно f a при a ∈ s и равно 1 при a ∉ s.

LaTeX

$$$mulIndicator\ s\ f\ a = \begin{cases} f\ a, & a \in s \\ 1, & a \notin s \end{cases}$$$

Lean4

@[to_additive]
theorem mulIndicator_apply (s : Set α) (f : α → M) (a : α) [Decidable (a ∈ s)] :
    mulIndicator s f a = if a ∈ s then f a else 1 :=
  by
  unfold mulIndicator
  congr

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