English
Given a clopen set U and a locally constant function f, MulIndicator f U is the locally constant function which equals f on U and equals 1 outside U.
Русский
Дано клип-множество U и локально константная функция f; MulIndicator f U равна f на U и единице вне U.
LaTeX
$$$ (f.mulIndicator\\ hU)(x) = \\begin{cases} f(x), & x \\in U; \\\\ 1, & x \\notin U. \\end{cases} $$$
Lean4
/-- Given a clopen set `U` and a locally constant function `f`, `LocallyConstant.mulIndicator`
returns the locally constant function that is `f` on `U` and `1` otherwise. -/
@[to_additive (attr := simps) /-- Given a clopen set `U` and a locally constant function `f`,
`LocallyConstant.indicator` returns the locally constant function that is `f` on `U` and `0`
otherwise. -/
]
noncomputable def mulIndicator (hU : IsClopen U) : LocallyConstant X R
where
toFun := Set.mulIndicator U f
isLocallyConstant := fun s => by
rw [mulIndicator_preimage, Set.ite, Set.diff_eq]
exact ((f.2 s).inter hU.isOpen).union ((IsLocallyConstant.const 1 s).inter hU.compl.isOpen)
