English
Let s be connected, f continuous on s, and f(z) ≠ 0 and f(z) ≠ π for all z ∈ s. Then for any x,y ∈ s, (f(y)).sign = (f(x)).sign.
Русский
Пусть s связано, f непрерывна на s и f(z) ≠ 0, π для всех z ∈ s. Тогда для любых x,y ∈ s значения f(y).sign и f(x).sign совпадают.
LaTeX
$$$ \operatorname{IsConnected}(s) \land \operatorname{ContinuousOn}(f,s) \land \forall z \in s, f(z) \neq 0 \land f(z) \neq \pi \land x \in s \land y \in s \Rightarrow (f(y)).\operatorname{sign} = (f(x)).\operatorname{sign} $$$
Lean4
/-- Suppose a function to angles is continuous on a connected set and never takes the values `0`
or `π` on that set. Then the values of the function on that set all have the same sign. -/
theorem sign_eq_of_continuousOn {α : Type*} [TopologicalSpace α] {f : α → Angle} {s : Set α} {x y : α}
(hc : IsConnected s) (hf : ContinuousOn f s) (hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ π) (hx : x ∈ s) (hy : y ∈ s) :
(f y).sign = (f x).sign :=
(hc.image _ (hf.angle_sign_comp hs)).isPreconnected.subsingleton (Set.mem_image_of_mem _ hy)
(Set.mem_image_of_mem _ hx)
