comp_mulIndicator — Mathlib

English

Let h: M → N and f: α → M. Then h(s.mulIndicator f(x)) equals the piecewise function that maps x to h(f(x)) on S and h(1) outside S.

Русский

Пусть h: M → N и f: α → M. Тогда h( (s.mulIndicator f)(x) ) равна функции в точке x, равной h(f(x)) при x ∈ S и h(1) при x ∉ S.

LaTeX

$$$h\\bigl(s.mulIndicator f\\,x\\bigr) = s.piecewise(h \\circ f)\n(\\text{const }\\alpha(h(1)))\\ x$$$

Lean4

@[to_additive]
theorem comp_mulIndicator (h : M → β) (f : α → M) {s : Set α} {x : α} [DecidablePred (· ∈ s)] :
    h (s.mulIndicator f x) = s.piecewise (h ∘ f) (const α (h 1)) x :=
  by
  letI := Classical.decPred (· ∈ s)
  convert s.apply_piecewise f (const α 1) (fun _ => h) (x := x) using 2

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