Theorems · Theorem · Lie groups

Real.Angle.sign_eq_of_continuousOn

∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → Real.Angle} {s : Set α} {x y : α},
  IsConnected s → ContinuousOn f s → (∀ z ∈ s, f z ≠ 0 ∧ f z ≠ ↑Real.pi) → x ∈ s → y ∈ s → (f y).sign = (f x).sign

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.

Defined in

Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle

Cited by

3 results in Mathlib

Foundations

Depth 190 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace