theorem helperForTheorem_6_8_continuous_selfMap_unitSphereTwo_exists_fixed_or_fixed_eq_antipode (g : UnitSphereTwo → UnitSphereTwo) : Continuous g → (∃ (x : UnitSphereTwo), g x = x) ∨ ∃ (x : UnitSphereTwo), g x = helperForTheorem_6_8_antipode x

Helper for Theorem 6.8: prerequisite global fixed-point-or-antipode-equality principle for continuous self-maps of S².

theorem helperForTheorem_6_8_continuous_selfMap_unitSphereTwo_no_counterexample_fixed_or_fixed_eq_antipode : ¬∃ (g : UnitSphereTwo → UnitSphereTwo), Continuous g ∧ ¬((∃ (x : UnitSphereTwo), g x = x) ∨ ∃ (x : UnitSphereTwo), g x = helperForTheorem_6_8_antipode x)

Helper for Theorem 6.8: prerequisite no-counterexample statement for continuous self-maps of S² in fixed-point-or-antipode-equality form.

theorem helperForTheorem_6_8_global_fixed_or_fixed_eq_antipode_of_no_counterexample_fixed_or_fixed_eq_antipode (hnoCounterexample : ¬∃ (g : UnitSphereTwo → UnitSphereTwo), Continuous g ∧ ¬((∃ (x : UnitSphereTwo), g x = x) ∨ ∃ (x : UnitSphereTwo), g x = helperForTheorem_6_8_antipode x)) (g : UnitSphereTwo → UnitSphereTwo) : Continuous g → (∃ (x : UnitSphereTwo), g x = x) ∨ ∃ (x : UnitSphereTwo), g x = helperForTheorem_6_8_antipode x

Helper for Theorem 6.8: the no-counterexample statement yields the corresponding global fixed-point-or-antipode-equality principle.

theorem helperForTheorem_6_8_global_exists_fixed_or_antifixed_of_no_counterexample_fixed_or_fixed_eq_antipode (hnoCounterexample : ¬∃ (g : UnitSphereTwo → UnitSphereTwo), Continuous g ∧ ¬((∃ (x : UnitSphereTwo), g x = x) ∨ ∃ (x : UnitSphereTwo), g x = helperForTheorem_6_8_antipode x)) (g : UnitSphereTwo → UnitSphereTwo) : Continuous g → ∃ (x : UnitSphereTwo), g x = x ∨ ↑(g x) = -↑x

Helper for Theorem 6.8: the no-counterexample statement in fixed-point-or- antipode-equality form yields the global fixed/anti-fixed existence principle.

theorem helperForTheorem_6_8_global_exists_fixed_or_antifixed_of_continuous_prereq (g : UnitSphereTwo → UnitSphereTwo) : Continuous g → ∃ (x : UnitSphereTwo), g x = x ∨ ↑(g x) = -↑x

Helper for Theorem 6.8: prerequisite global fixed/anti-fixed existence for continuous self-maps of S².

theorem helperForTheorem_6_8_exists_fixed_or_antifixed_of_continuous_of_global_exists_fixed_or_antifixed_principle (hprinciple : ∀ (g : UnitSphereTwo → UnitSphereTwo), Continuous g → ∃ (x : UnitSphereTwo), g x = x ∨ ↑(g x) = -↑x) (f : UnitSphereTwo → UnitSphereTwo) (hcont : Continuous f) : ∃ (x : UnitSphereTwo), f x = x ∨ ↑(f x) = -↑x

Helper for Theorem 6.8: a global fixed/anti-fixed existence principle directly yields the local fixed/anti-fixed witness for any continuous self-map of S².

theorem helperForTheorem_6_8_exists_fixed_or_antifixed_of_continuous_of_global_fixed_or_antipode_comp_fixed_principle (hprinciple : ∀ (g : UnitSphereTwo → UnitSphereTwo), Continuous g → (∃ (x : UnitSphereTwo), g x = x) ∨ ∃ (x : UnitSphereTwo), helperForTheorem_6_8_antipode (g x) = x) (f : UnitSphereTwo → UnitSphereTwo) (hcont : Continuous f) : ∃ (x : UnitSphereTwo), f x = x ∨ ↑(f x) = -↑x

Helper for Theorem 6.8: a global fixed-point-or-antipode-composed-fixed principle directly yields the local fixed/anti-fixed witness for any continuous self-map of S².

theorem helperForTheorem_6_8_global_exists_fixed_or_antifixed_of_global_fixed_or_antipode_comp_fixed_principle (hprinciple : ∀ (g : UnitSphereTwo → UnitSphereTwo), Continuous g → (∃ (x : UnitSphereTwo), g x = x) ∨ ∃ (x : UnitSphereTwo), helperForTheorem_6_8_antipode (g x) = x) (g : UnitSphereTwo → UnitSphereTwo) : Continuous g → ∃ (x : UnitSphereTwo), g x = x ∨ ↑(g x) = -↑x

Helper for Theorem 6.8: a global fixed-point-or-antipode-composed-fixed principle on continuous self-maps of S² implies the global fixed/anti-fixed existence principle.

theorem helperForTheorem_6_8_fixed_or_fixed_eq_antipode_of_continuous_prereq (f : UnitSphereTwo → UnitSphereTwo) (hcont : Continuous f) : (∃ (x : UnitSphereTwo), f x = x) ∨ ∃ (x : UnitSphereTwo), f x = helperForTheorem_6_8_antipode x

Helper for Theorem 6.8: prerequisite fixed-point/antipode-equality alternative on S² derived from continuity.

theorem helperForTheorem_6_8_exists_fixed_or_antifixed_of_continuous (f : UnitSphereTwo → UnitSphereTwo) (hcont : Continuous f) : ∃ (x : UnitSphereTwo), f x = x ∨ ↑(f x) = -↑x

Helper for Theorem 6.8: upstream fixed/anti-fixed existence for continuous self-maps of S².

theorem helperForTheorem_6_8_fixed_or_fixed_eq_antipode_of_continuous (f : UnitSphereTwo → UnitSphereTwo) (hcont : Continuous f) : (∃ (x : UnitSphereTwo), f x = x) ∨ ∃ (x : UnitSphereTwo), f x = helperForTheorem_6_8_antipode x

Helper for Theorem 6.8: topological fixed-point/antipode-equality existence from continuity on S².

theorem helperForTheorem_6_8_fixed_or_antipode_comp_fixed_prereq (f : UnitSphereTwo → UnitSphereTwo) (hcont : Continuous f) : (∃ (x : UnitSphereTwo), f x = x) ∨ ∃ (x : UnitSphereTwo), helperForTheorem_6_8_antipode (f x) = x

Helper for Theorem 6.8: prerequisite fixed-point/antipode-fixed alternative on S².

theorem hairy_ball_fixed_or_antifixed_alternative_6_8 (f : UnitSphereTwo → UnitSphereTwo) (hcont : Continuous f) : ∃ (x : UnitSphereTwo), f x = x ∨ ↑(f x) = -↑x

Theorem 6.8 (Hairy ball theorem, fixed point/anti-fixed point alternative): for any continuous self-map f : S² → S², there exists x ∈ S² such that either f x = x or f x = -x (expressed on ambient vectors).

theorem origin_mem_ball_origin_of_pos {n : ℕ} {r : ℝ} (hr : 0 < r) : 0 ∈ Metric.ball 0 r

The origin belongs to the open ball centered at the origin with positive radius.

theorem contraction_perturbation_injective_and_ball_half_subset_range {n : ℕ} {r : ℝ} (hr : 0 < r) (g : ↑(Metric.ball 0 r) → EuclideanSpace ℝ (Fin n)) (hzero : g ⟨0, ⋯⟩ = 0) (hcontract : ∀ (x y : ↑(Metric.ball 0 r)), ‖g x - g y‖ ≤ 1 / 2 * ‖↑x - ↑y‖) : (Function.Injective fun (x : ↑(Metric.ball 0 r)) => ↑x + g x) ∧ Metric.ball 0 (r / 2) ⊆ Set.range fun (x : ↑(Metric.ball 0 r)) => ↑x + g x

Lemma 6.7: Let r > 0 and let g : B(0,r) → ℝ^n satisfy g(0) = 0 and ‖g(x) - g(y)‖ ≤ (1/2) ‖x - y‖ for all x,y ∈ B(0,r). If f(x) = x + g(x) on B(0,r), then f is injective and B(0,r/2) ⊆ f(B(0,r)).