English
If f is continuous on a set s and f(z) ≠ 0 and f(z) ≠ π for all z ∈ s, then the composed function x ↦ sign(f(x)) is continuous on s.
Русский
Пусть f непрерывна на s и для всех z ∈ s выполняется f(z) ≠ 0 и f(z) ≠ π; тогда x ↦ sign(f(x)) непрерывна на s.
LaTeX
$$$ \big( \operatorname{ContinuousOn} f s \big) \land \big( \forall z \in s, f(z) \neq 0 \land f(z) \neq \pi \big) \Rightarrow \operatorname{ContinuousOn}(\operatorname{sign} \circ f, s) $$$
Lean4
theorem _root_.ContinuousOn.angle_sign_comp {α : Type*} [TopologicalSpace α] {f : α → Angle} {s : Set α}
(hf : ContinuousOn f s) (hs : ∀ z ∈ s, f z ≠ 0 ∧ f z ≠ π) : ContinuousOn (sign ∘ f) s :=
by
refine (continuousOn_of_forall_continuousAt fun θ hθ => ?_).comp hf (Set.mapsTo_image f s)
obtain ⟨z, hz, rfl⟩ := hθ
exact continuousAt_sign (hs _ hz).1 (hs _ hz).2
