mulIndicator — Mathlib

English

Set.mulIndicator s f x equals f(x) if x ∈ s, and equals 1 otherwise.

Русский

Set.mulIndicator s f x равняется f(x) если x ∈ s, и 1 в противном случае.

LaTeX

$$$$\mathrm{mulIndicator}(s,f,x) = \begin{cases} f(x), & x \in s \\ 1, & x \notin s \end{cases}.$$$$

Lean4

/-- `Set.mulIndicator s f a` is `f a` if `a ∈ s`, `1` otherwise. -/
@[to_additive /-- `Set.indicator s f a` is `f a` if `a ∈ s`, `0` otherwise. -/
    ]
noncomputable def mulIndicator (s : Set α) (f : α → M) (x : α) : M :=
  haveI := Classical.decPred (· ∈ s)
  if x ∈ s then f x else 1

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