Helper for Theorem 6.8: S² is connected as a topological space.
theorem
helperForTheorem_6_8_odd_sub_antipode
{α : Type u_1}
[AddGroup α]
(g : UnitSphereTwo → α)
:
Function.Odd fun (x : UnitSphereTwo) => g x - g (-x)
Helper for Theorem 6.8: for any additive codomain, the map
x ↦ g x - g (-x) is odd on S².
theorem
helperForTheorem_6_8_continuous_sub_antipode
{α : Type u_1}
[TopologicalSpace α]
[AddGroup α]
[ContinuousAdd α]
[ContinuousNeg α]
(g : UnitSphereTwo → α)
(hg : Continuous g)
:
Continuous fun (x : UnitSphereTwo) => g x - g (-x)
Helper for Theorem 6.8: continuity of x ↦ g x - g (-x) follows from
continuity of g.
theorem
helperForTheorem_6_8_continuous_real_exists_antipodal_equal
(g : UnitSphereTwo → ℝ)
(hg : Continuous g)
:
∃ (x : UnitSphereTwo), g x = g (-x)
Helper for Theorem 6.8: every continuous real-valued map on S² takes equal
values at some antipodal pair.
theorem
helperForTheorem_6_8_continuous_odd_real_exists_zero
(h : UnitSphereTwo → ℝ)
(hcont : Continuous h)
(hodd : ∀ (x : UnitSphereTwo), h (-x) = -h x)
:
∃ (x : UnitSphereTwo), h x = 0
Helper for Theorem 6.8: an odd continuous real-valued map on S² has a zero.