mulIndicator_eq_one_or_self — Mathlib

English

For any a, mulIndicator s f a equals 1 or equals f a.

Русский

Для любого a выполняется, что mulIndicator s f a равно 1 или равно f a.

LaTeX

$$mulIndicator s f a = 1 ∨ mulIndicator s f a = f a$$

Lean4

@[to_additive]
theorem mulIndicator_eq_one_or_self (s : Set α) (f : α → M) (a : α) :
    mulIndicator s f a = 1 ∨ mulIndicator s f a = f a :=
  by
  by_cases h : a ∈ s
  · exact Or.inr (mulIndicator_of_mem h f)
  · exact Or.inl (mulIndicator_of_notMem h f)

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