theorem
ContinuousOn.sign
{α : Type u_1}
[Zero α]
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{β : Type u_2}
[TopologicalSpace β]
{f : β → α}
{s : Set β}
(hf : ContinuousOn f s)
(h0 : ∀ x ∈ s, f x ≠ 0)
:
ContinuousOn (fun (x : β) => SignType.sign (f x)) s
The sign of a continuous function is continuous wherever the function is nonzero.
theorem
IsPreconnected.sign_eq_of_continuousOn
{α : Type u_1}
[Zero α]
[TopologicalSpace α]
[LinearOrder α]
[OrderTopology α]
{β : Type u_2}
[TopologicalSpace β]
{f : β → α}
{s : Set β}
(hs : IsPreconnected s)
(hf : ContinuousOn f s)
(h0 : ∀ x ∈ s, f x ≠ 0)
{x y : β}
(hx : x ∈ s)
(hy : y ∈ s)
:
A continuous nonvanishing function has constant sign on a preconnected set.