Continuity of indicator functions #
theorem
continuous_mulIndicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{s : Set α}
[One β]
(hs : ∀ a ∈ frontier s, f a = 1)
(hf : ContinuousOn f (closure s))
:
Continuous (s.mulIndicator f)
theorem
continuous_indicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{s : Set α}
[Zero β]
(hs : ∀ a ∈ frontier s, f a = 0)
(hf : ContinuousOn f (closure s))
:
Continuous (s.indicator f)
theorem
Continuous.mulIndicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{s : Set α}
[One β]
(hs : ∀ a ∈ frontier s, f a = 1)
(hf : Continuous f)
:
Continuous (s.mulIndicator f)
theorem
Continuous.indicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{s : Set α}
[Zero β]
(hs : ∀ a ∈ frontier s, f a = 0)
(hf : Continuous f)
:
Continuous (s.indicator f)
theorem
ContinuousOn.continuousAt_mulIndicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{s : Set α}
[One β]
(hf : ContinuousOn f (interior s))
{x : α}
(hx : x ∉ frontier s)
:
ContinuousAt (s.mulIndicator f) x
theorem
ContinuousOn.continuousAt_indicator
{α : Type u_1}
{β : Type u_2}
[TopologicalSpace α]
[TopologicalSpace β]
{f : α → β}
{s : Set α}
[Zero β]
(hf : ContinuousOn f (interior s))
{x : α}
(hx : x ∉ frontier s)
:
ContinuousAt (s.indicator f) x