English
If f is continuous on interior s and x is not on the frontier of s, then s.mulIndicator f is continuous at x.
Русский
Если f непрерывна внутри s и x не лежит на границе s, то s.mulIndicator f непрерывна в точке x.
LaTeX
$$$\\forall x, x \\notin \\text{frontier}(s) \\Rightarrow \\text{ContinuousAt}(s.mulIndicator f) x$$$
Lean4
@[to_additive]
theorem continuousAt_mulIndicator (hf : ContinuousOn f (interior s)) {x : α} (hx : x ∉ frontier s) :
ContinuousAt (s.mulIndicator f) x :=
by
rw [← Set.mem_compl_iff, compl_frontier_eq_union_interior] at hx
obtain h | h := hx
· have hs : interior s ∈ 𝓝 x := mem_interior_iff_mem_nhds.mp (by rwa [interior_interior])
exact
ContinuousAt.congr (hf.continuousAt hs) <|
Filter.eventuallyEq_iff_exists_mem.mpr ⟨interior s, hs, Set.eqOn_mulIndicator.symm.mono interior_subset⟩
·
exact
ContinuousAt.congr continuousAt_const <|
Filter.eventuallyEq_iff_exists_mem.mpr ⟨sᶜ, mem_interior_iff_mem_nhds.mp h, Set.eqOn_mulIndicator'.symm⟩
