def IsContraction {X : Type u_1} [MetricSpace X] (f : X → X) : Prop

A self-map f : X → X is a contraction if it is 1-Lipschitz.

Equations

• IsContraction f = ∀ (x y : X), dist (f x) (f y) ≤ dist x y

def IsStrictContraction {X : Type u_1} [MetricSpace X] (f : X → X) : Prop

A self-map f : X → X is a strict contraction if it has a contraction constant c with 0 < c < 1.

Equations

• IsStrictContraction f = ∃ (c : ℝ), 0 < c ∧ c < 1 ∧ ∀ (x y : X), dist (f x) (f y) ≤ c * dist x y

def IsContractionConstant {X : Type u_1} [MetricSpace X] (f : X → X) (c : ℝ) : Prop

A real number c is a contraction constant of f if 0 < c < 1 and dist (f x) (f y) ≤ c * dist x y for all x,y.

Equations

• IsContractionConstant f c = (0 < c ∧ c < 1 ∧ ∀ (x y : X), dist (f x) (f y) ≤ c * dist x y)

theorem definition_6_13 {X : Type u_1} [MetricSpace X] (f : X → X) : (IsContraction f ↔ ∀ (x y : X), dist (f x) (f y) ≤ dist x y) ∧ (IsStrictContraction f ↔ ∃ (c : ℝ), IsContractionConstant f c)

Definition 6.13 (Contraction and strict contraction): (i) f is a contraction iff dist (f x) (f y) ≤ dist x y for all x,y. (ii) f is a strict contraction iff there exists c with 0 < c < 1 such that dist (f x) (f y) ≤ c * dist x y for all x,y; such a c is a contraction constant.

theorem deriv_bound_one_on_interval_implies_nonexpanding {a b : ℝ} (f : ℝ → ℝ) (hmaps : Set.MapsTo f (Set.Icc a b) (Set.Icc a b)) (hcont : ContinuousOn f (Set.Icc a b)) (hdiff : DifferentiableOn ℝ f (Set.Ioo a b)) (hderiv : ∀ x ∈ Set.Ioo a b, |deriv f x| ≤ 1) : (∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc a b, |f x - f y| ≤ |x - y|) ∧ IsContraction (Set.MapsTo.restrict f (Set.Icc a b) (Set.Icc a b) hmaps)

Proposition 6.13(1): if f : [a,b] → [a,b] is continuous on [a,b], differentiable on (a,b), and |f'| ≤ 1 on (a,b), then |f(x) - f(y)| ≤ |x - y| for all x,y ∈ [a,b]; in particular, the induced self-map of [a,b] is a non-expanding contraction.

theorem contraction_on_interval_implies_deriv_bound_one {a b : ℝ} (f : ℝ → ℝ) (hdiff : DifferentiableOn ℝ f (Set.Icc a b)) (hcontract : ∀ x ∈ Set.Icc a b, ∀ y ∈ Set.Icc a b, |f x - f y| ≤ |x - y|) (x : ℝ) : x ∈ Set.Icc a b → |derivWithin f (Set.Icc a b) x| ≤ 1

Proposition 6.14: Let f : [a,b] → ℝ be differentiable and assume |f x - f y| ≤ |x - y| for all x,y ∈ [a,b]. Then the derivative of f within [a,b] satisfies |f'(x)| ≤ 1 for all x ∈ [a,b].

theorem helperForProposition_6_15_unpack_nonneg_bound {X : Type u_1} [MetricSpace X] (f : X → X) (hcontract : ∃ (c : ℝ), 0 ≤ c ∧ c < 1 ∧ ∀ (x y : X), dist (f x) (f y) ≤ c * dist x y) : ∃ (c : ℝ), 0 ≤ c ∧ ∀ (x y : X), dist (f x) (f y) ≤ c * dist x y

Helper for Proposition 6.15: from a contraction witness with 0 ≤ c < 1, extract the nonnegativity and distance bound needed for Lipschitz control.

theorem helperForProposition_6_15_lipschitzWith_of_real_contraction_bound {X : Type u_1} [MetricSpace X] (f : X → X) (hbound : ∃ (c : ℝ), 0 ≤ c ∧ ∀ (x y : X), dist (f x) (f y) ≤ c * dist x y) : ∃ (K : NNReal), LipschitzWith K f

Helper for Proposition 6.15: convert a real-valued contraction estimate with c ≥ 0 into an NNReal-valued LipschitzWith bound.

theorem helperForProposition_6_15_continuous_of_exists_lipschitzWith {X : Type u_1} [MetricSpace X] (f : X → X) (hlip : ∃ (K : NNReal), LipschitzWith K f) : Continuous f

Helper for Proposition 6.15: any map with an NNReal Lipschitz bound is continuous.

theorem contraction_has_lipschitz_and_continuous {X : Type u_1} [MetricSpace X] (f : X → X) (hcontract : ∃ (c : ℝ), 0 ≤ c ∧ c < 1 ∧ ∀ (x y : X), dist (f x) (f y) ≤ c * dist x y) : (∃ (K : NNReal), LipschitzWith K f) ∧ Continuous f

Proposition 6.15: If f : X → X on a metric space satisfies dist (f x) (f y) ≤ c * dist x y for some c ∈ [0,1) and all x,y, then f is Lipschitz and therefore continuous on X.

def IsFixedPoint {X : Type u_1} (f : X → X) (x : X) : Prop

Definition 6.14 (Fixed point): Let X be a set and let f : X → X be a map. An element x ∈ X is a fixed point of f if f x = x.

Equations

• IsFixedPoint f x = (f x = x)

theorem helperForTheorem_6_7_contractingWith_of_nonneg_constant {X : Type u_1} [MetricSpace X] (f : X → X) (hstrict : ∃ (c : ℝ), 0 ≤ c ∧ c < 1 ∧ ∀ (x y : X), dist (f x) (f y) ≤ c * dist x y) : ∃ (K : NNReal), ContractingWith K f

Helper for Theorem 6.7: convert a real-valued contraction bound with 0 ≤ c < 1 into ContractingWith with an NNReal constant.

theorem helperForTheorem_6_7_fixedPoint_eq_of_contractingWith {X : Type u_1} [MetricSpace X] {f : X → X} {K : NNReal} (hfK : ContractingWith K f) {x y : X} (hx : IsFixedPoint f x) (hy : IsFixedPoint f y) : x = y

Helper for Theorem 6.7: fixed points of a ContractingWith map are unique.

theorem helperForTheorem_6_7_existsUnique_fixedPoint_of_contractingWith {X : Type u_1} [MetricSpace X] [Nonempty X] [CompleteSpace X] {f : X → X} {K : NNReal} (hfK : ContractingWith K f) : ∃! x : X, IsFixedPoint f x

Helper for Theorem 6.7: in a nonempty complete metric space, a ContractingWith map has a unique fixed point.

theorem contraction_mapping_theorem_6_7 {X : Type u_1} [MetricSpace X] (f : X → X) (hstrict : ∃ (c : ℝ), 0 ≤ c ∧ c < 1 ∧ ∀ (x y : X), dist (f x) (f y) ≤ c * dist x y) : (∀ (x y : X), IsFixedPoint f x → IsFixedPoint f y → x = y) ∧ (Nonempty X → CompleteSpace X → ∃! x : X, IsFixedPoint f x)

Theorem 6.7 (Contraction mapping theorem): Let (X,d) be a metric space and f : X → X satisfy dist (f x) (f y) ≤ c * dist x y for some c ∈ [0,1) and all x,y. Then f has at most one fixed point. If, in addition, X is nonempty and complete, then f has exactly one fixed point.

theorem helperForProposition_6_16_dist_le_eps_add_c_mul_dist {X : Type u_1} [MetricSpace X] (f g : X → X) (c : ℝ) (x0 y0 : X) (ε : ℝ) (hf : IsContractionConstant f c) (hx0 : IsFixedPoint f x0) (hy0 : IsFixedPoint g y0) (hclose : ∀ (x : X), dist (f x) (g x) ≤ ε) : dist x0 y0 ≤ ε + c * dist x0 y0

Helper for Proposition 6.16: the f-centered triangle inequality and contraction bound imply dist x0 y0 ≤ ε + c * dist x0 y0.

theorem helperForProposition_6_16_dist_le_eps_add_cprime_mul_dist {X : Type u_1} [MetricSpace X] (f g : X → X) (c' : ℝ) (x0 y0 : X) (ε : ℝ) (hg : IsContractionConstant g c') (hx0 : IsFixedPoint f x0) (hy0 : IsFixedPoint g y0) (hclose : ∀ (x : X), dist (f x) (g x) ≤ ε) : dist x0 y0 ≤ ε + c' * dist x0 y0

Helper for Proposition 6.16: the g-centered triangle inequality and contraction bound imply dist x0 y0 ≤ ε + c' * dist x0 y0.

theorem helperForProposition_6_16_le_div_one_sub_of_le_add_mul (d ε a : ℝ) (ha1 : a < 1) (hd : d ≤ ε + a * d) : d ≤ ε / (1 - a)

Helper for Proposition 6.16: from d ≤ ε + a*d with a < 1, one gets d ≤ ε / (1 - a).

theorem helperForProposition_6_16_min_case_finish (d ε c c' : ℝ) (h1 : d ≤ ε / (1 - c)) (h2 : d ≤ ε / (1 - c')) : d ≤ ε / (1 - min c c')

Helper for Proposition 6.16: combine the c- and c'-division bounds into the denominator 1 - min c c' by a case split on c ≤ c'.

theorem fixed_point_distance_le_of_uniformly_close_strict_contractions {X : Type u_1} [MetricSpace X] [CompleteSpace X] (f g : X → X) (c c' : ℝ) (x0 y0 : X) (ε : ℝ) (hf : IsContractionConstant f c) (hg : IsContractionConstant g c') (hx0 : IsFixedPoint f x0) (hy0 : IsFixedPoint g y0) (hε : 0 < ε) (hclose : ∀ (x : X), dist (f x) (g x) ≤ ε) : dist x0 y0 ≤ ε / (1 - min c c')

Proposition 6.16: Let (X,d) be a complete metric space, and let f,g : X → X be strict contractions with contraction constants c,c' ∈ (0,1), respectively. If x₀ and y₀ are fixed points of f and g, and there exists ε > 0 such that dist (f x) (g x) ≤ ε for all x, then dist x₀ y₀ ≤ ε / (1 - min c c').

theorem helperForTheorem_6_6_contractingWith_of_real_constant {X : Type u_1} [MetricSpace X] (f : X → X) (hcontract : ∃ (c : ℝ), 0 < c ∧ c < 1 ∧ ∀ (x y : X), dist (f x) (f y) ≤ c * dist x y) : ∃ (K : NNReal), ContractingWith K f

Helper for Theorem 6.6: turn the real-valued contraction hypothesis into ContractingWith with an NNReal constant.

theorem helperForTheorem_6_6_isFixedPoint_iff_isFixedPt {X : Type u_1} (f : X → X) (x : X) : IsFixedPoint f x ↔ Function.IsFixedPt f x

Helper for Theorem 6.6: the local fixed-point predicate agrees with mathlib's IsFixedPt.

theorem helperForTheorem_6_6_unique_at_mathlib_fixedPoint {X : Type u_1} [MetricSpace X] [CompleteSpace X] [Nonempty X] {f : X → X} {K : NNReal} (hfK : ContractingWith K f) (y : X) : IsFixedPoint f y → y = ContractingWith.fixedPoint f hfK

Helper for Theorem 6.6: uniqueness stated using ContractingWith.fixedPoint.

theorem helperForTheorem_6_6_tendsto_nat_iterate_fixedPoint {X : Type u_1} [MetricSpace X] [CompleteSpace X] [Nonempty X] {f : X → X} {K : NNReal} (hfK : ContractingWith K f) (x0 : X) : Filter.Tendsto (fun (n : ℕ) => f^[n] x0) Filter.atTop (nhds (ContractingWith.fixedPoint f hfK))

Helper for Theorem 6.6: iterates Nat.iterate f n x₀ converge to the ContractingWith.fixedPoint.

theorem banach_fixed_point_theorem {X : Type u_1} [MetricSpace X] [CompleteSpace X] [Nonempty X] (f : X → X) (hcontract : ∃ (c : ℝ), 0 < c ∧ c < 1 ∧ ∀ (x y : X), dist (f x) (f y) ≤ c * dist x y) : ∃ (xstar : X), IsFixedPoint f xstar ∧ (∀ (y : X), IsFixedPoint f y → y = xstar) ∧ ∀ (x0 : X), Filter.Tendsto (fun (n : ℕ) => f^[n] x0) Filter.atTop (nhds xstar)

Theorem 6.6 (Banach fixed-point theorem): If X is a nonempty complete metric space and f : X → X is a contraction with constant c satisfying 0 < c < 1, then f has a unique fixed point x*; moreover, for every initial point x₀, the iterates x_{n+1} = f(x_n) converge to x*.

@[reducible, inline]

abbrev UnitSphereTwo : Type

The unit 2-sphere in ℝ^3, viewed as a subtype of EuclideanSpace ℝ (Fin 3).

Equations

• UnitSphereTwo = { x : EuclideanSpace ℝ (Fin 3) // x ∈ Metric.sphere 0 1 }

theorem helperForTheorem_6_8_neg_mem_unitSphereTwo (x : UnitSphereTwo) : -↑x ∈ Metric.sphere 0 1

Helper for Theorem 6.8: the antipode of a point on S² still lies on S².

theorem helperForTheorem_6_8_exists_antipode (x : UnitSphereTwo) : ∃ (y : UnitSphereTwo), ↑y = -↑x

Helper for Theorem 6.8: every point of S² has an antipodal point in S².

theorem helperForTheorem_6_8_ne_self_neg (x : UnitSphereTwo) : ↑x ≠ -↑x

Helper for Theorem 6.8: no point on S² is equal to its antipode.

noncomputable def helperForTheorem_6_8_antipode (point : UnitSphereTwo) : UnitSphereTwo

Helper for Theorem 6.8: the antipode self-map on S².

Equations

• helperForTheorem_6_8_antipode point = -point

theorem helperForTheorem_6_8_continuous_antipode : Continuous helperForTheorem_6_8_antipode

Helper for Theorem 6.8: the antipode map on S² is continuous.

theorem helperForTheorem_6_8_antipode_involutive (x : UnitSphereTwo) : helperForTheorem_6_8_antipode (helperForTheorem_6_8_antipode x) = x

Helper for Theorem 6.8: applying the antipode map twice gives the original point.

theorem helperForTheorem_6_8_antipode_comp_fixed_iff_fixed_eq_antipode {f : UnitSphereTwo → UnitSphereTwo} {x : UnitSphereTwo} : helperForTheorem_6_8_antipode (f x) = x ↔ f x = helperForTheorem_6_8_antipode x

Helper for Theorem 6.8: fixed points of antipode ∘ f are exactly points where f agrees with the antipode map.

theorem helperForTheorem_6_8_fixed_eq_antipode_iff_antifixed {f : UnitSphereTwo → UnitSphereTwo} {x : UnitSphereTwo} : f x = helperForTheorem_6_8_antipode x ↔ ↑(f x) = -↑x

Helper for Theorem 6.8: f x = antipode x is equivalent to the ambient anti-fixed equation (f x).1 = -x.1.

theorem helperForTheorem_6_8_exists_antifixed_of_exists_fixed_eq_antipode {f : UnitSphereTwo → UnitSphereTwo} (h : ∃ (x : UnitSphereTwo), f x = helperForTheorem_6_8_antipode x) : ∃ (x : UnitSphereTwo), ↑(f x) = -↑x

Helper for Theorem 6.8: if f x = antipode x for some x, then f has an ambient anti-fixed point.

theorem helperForTheorem_6_8_exists_fixed_eq_antipode_of_exists_antifixed {f : UnitSphereTwo → UnitSphereTwo} (h : ∃ (x : UnitSphereTwo), ↑(f x) = -↑x) : ∃ (x : UnitSphereTwo), f x = helperForTheorem_6_8_antipode x

Helper for Theorem 6.8: if f has an ambient anti-fixed point, then f agrees with antipode at some point.

theorem helperForTheorem_6_8_exists_fixed_eq_antipode_iff_exists_antifixed {f : UnitSphereTwo → UnitSphereTwo} : (∃ (x : UnitSphereTwo), f x = helperForTheorem_6_8_antipode x) ↔ ∃ (x : UnitSphereTwo), ↑(f x) = -↑x

Helper for Theorem 6.8: existence of a point with f x = antipode x is equivalent to existence of an ambient anti-fixed point.

theorem helperForTheorem_6_8_exists_of_fixed_or_fixed_eq_antipode {f : UnitSphereTwo → UnitSphereTwo} (h : (∃ (x : UnitSphereTwo), f x = x) ∨ ∃ (x : UnitSphereTwo), f x = helperForTheorem_6_8_antipode x) : ∃ (x : UnitSphereTwo), f x = x ∨ ↑(f x) = -↑x

Helper for Theorem 6.8: from a fixed point or a point with f x = antipode x, one obtains the theorem's fixed/anti-fixed alternative.

theorem helperForTheorem_6_8_exists_antipode_comp_fixed_iff_exists_fixed_eq_antipode {f : UnitSphereTwo → UnitSphereTwo} : (∃ (x : UnitSphereTwo), helperForTheorem_6_8_antipode (f x) = x) ↔ ∃ (x : UnitSphereTwo), f x = helperForTheorem_6_8_antipode x

Helper for Theorem 6.8: existence of a fixed point of antipode ∘ f is equivalent to existence of a point with f x = antipode x.

theorem helperForTheorem_6_8_exists_antipode_comp_fixed_iff_exists_antifixed {f : UnitSphereTwo → UnitSphereTwo} : (∃ (x : UnitSphereTwo), helperForTheorem_6_8_antipode (f x) = x) ↔ ∃ (x : UnitSphereTwo), ↑(f x) = -↑x

Helper for Theorem 6.8: existence of a fixed point of antipode ∘ f is equivalent to existence of an ambient anti-fixed point.

theorem helperForTheorem_6_8_fixed_or_fixed_eq_antipode_iff_fixed_or_antipode_comp_fixed {f : UnitSphereTwo → UnitSphereTwo} : ((∃ (x : UnitSphereTwo), f x = x) ∨ ∃ (x : UnitSphereTwo), f x = helperForTheorem_6_8_antipode x) ↔ (∃ (x : UnitSphereTwo), f x = x) ∨ ∃ (x : UnitSphereTwo), helperForTheorem_6_8_antipode (f x) = x

Helper for Theorem 6.8: rewriting the second disjunct between f x = antipode x and fixed points of antipode ∘ f.

theorem helperForTheorem_6_8_fixed_or_antipode_comp_fixed_of_fixed_or_fixed_eq_antipode {f : UnitSphereTwo → UnitSphereTwo} (h : (∃ (x : UnitSphereTwo), f x = x) ∨ ∃ (x : UnitSphereTwo), f x = helperForTheorem_6_8_antipode x) : (∃ (x : UnitSphereTwo), f x = x) ∨ ∃ (x : UnitSphereTwo), helperForTheorem_6_8_antipode (f x) = x

Helper for Theorem 6.8: convert the fixed-or-antipode-equality disjunction into the fixed-or-antipode ∘ f-fixed disjunction.

theorem helperForTheorem_6_8_antifixed_of_antipode_comp_fixed {f : UnitSphereTwo → UnitSphereTwo} {x : UnitSphereTwo} (hfixed : helperForTheorem_6_8_antipode (f x) = x) : ↑(f x) = -↑x

Helper for Theorem 6.8: a fixed point of antipode ∘ f gives an anti-fixed point of f.

theorem helperForTheorem_6_8_antipode_comp_fixed_iff_antifixed {f : UnitSphereTwo → UnitSphereTwo} {x : UnitSphereTwo} : helperForTheorem_6_8_antipode (f x) = x ↔ ↑(f x) = -↑x

Helper for Theorem 6.8: anti-fixed points are exactly fixed points of antipode ∘ f.

theorem helperForTheorem_6_8_continuous_antipode_comp {f : UnitSphereTwo → UnitSphereTwo} (hcont : Continuous f) : Continuous fun (x : UnitSphereTwo) => helperForTheorem_6_8_antipode (f x)

Helper for Theorem 6.8: if f is continuous then antipode ∘ f is continuous.

theorem helperForTheorem_6_8_exists_of_fixed_or_antipode_comp_fixed {f : UnitSphereTwo → UnitSphereTwo} (h : (∃ (x : UnitSphereTwo), f x = x) ∨ ∃ (x : UnitSphereTwo), helperForTheorem_6_8_antipode (f x) = x) : ∃ (x : UnitSphereTwo), f x = x ∨ ↑(f x) = -↑x

Helper for Theorem 6.8: if f or antipode ∘ f has a fixed point, then the theorem's fixed/anti-fixed alternative follows.

theorem helperForTheorem_6_8_exists_fixed_or_antifixed_iff_fixed_or_fixed_eq_antipode {f : UnitSphereTwo → UnitSphereTwo} : (∃ (x : UnitSphereTwo), f x = x ∨ ↑(f x) = -↑x) ↔ (∃ (x : UnitSphereTwo), f x = x) ∨ ∃ (x : UnitSphereTwo), f x = helperForTheorem_6_8_antipode x

Helper for Theorem 6.8: the target fixed/anti-fixed-point existence statement is equivalent to the disjunction of a fixed point or a point where f equals antipode.

theorem helperForTheorem_6_8_exists_fixed_or_antifixed_iff_fixed_or_antipode_comp_fixed {f : UnitSphereTwo → UnitSphereTwo} : (∃ (x : UnitSphereTwo), f x = x ∨ ↑(f x) = -↑x) ↔ (∃ (x : UnitSphereTwo), f x = x) ∨ ∃ (x : UnitSphereTwo), helperForTheorem_6_8_antipode (f x) = x

Helper for Theorem 6.8: the target fixed/anti-fixed-point existence statement is equivalent to the disjunction of a fixed point of f or of antipode ∘ f.

theorem helperForTheorem_6_8_fixed_or_antipode_comp_fixed_of_exists_fixed_or_antifixed {f : UnitSphereTwo → UnitSphereTwo} (h : ∃ (x : UnitSphereTwo), f x = x ∨ ↑(f x) = -↑x) : (∃ (x : UnitSphereTwo), f x = x) ∨ ∃ (x : UnitSphereTwo), helperForTheorem_6_8_antipode (f x) = x

Helper for Theorem 6.8: an established fixed/anti-fixed witness yields the fixed-or-antipode- fixed disjunction.

theorem helperForTheorem_6_8_fixed_or_fixed_eq_antipode_of_exists_fixed_or_antifixed {f : UnitSphereTwo → UnitSphereTwo} (h : ∃ (x : UnitSphereTwo), f x = x ∨ ↑(f x) = -↑x) : (∃ (x : UnitSphereTwo), f x = x) ∨ ∃ (x : UnitSphereTwo), f x = helperForTheorem_6_8_antipode x

Helper for Theorem 6.8: an established fixed/anti-fixed witness yields the fixed-or-antipode- equality disjunction.

theorem helperForTheorem_6_8_exists_fixed_or_antifixed_of_exists_fixed {f : UnitSphereTwo → UnitSphereTwo} (hfixed : ∃ (x : UnitSphereTwo), f x = x) : ∃ (x : UnitSphereTwo), f x = x ∨ ↑(f x) = -↑x

Helper for Theorem 6.8: any fixed point of f directly gives a witness for the target fixed/anti-fixed alternative.

theorem helperForTheorem_6_8_exists_fixed_or_antifixed_of_exists_fixed_eq_antipode {f : UnitSphereTwo → UnitSphereTwo} (hantipode : ∃ (x : UnitSphereTwo), f x = helperForTheorem_6_8_antipode x) : ∃ (x : UnitSphereTwo), f x = x ∨ ↑(f x) = -↑x

Helper for Theorem 6.8: if f agrees with antipode at some point, then we obtain the target fixed/anti-fixed alternative witness.

theorem helperForTheorem_6_8_exists_of_fixed_or_antifixed {f : UnitSphereTwo → UnitSphereTwo} (h : (∃ (x : UnitSphereTwo), f x = x) ∨ ∃ (x : UnitSphereTwo), ↑(f x) = -↑x) : ∃ (x : UnitSphereTwo), f x = x ∨ ↑(f x) = -↑x

Helper for Theorem 6.8: from a disjunction of existence of a fixed point or of an ambient anti-fixed point, obtain a direct witness of the target existential alternative.

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

Helper for Theorem 6.8: any upstream principle asserting fixed-point-or-antipode- equality for continuous self-maps of S² yields the target fixed/anti-fixed alternative.

theorem helperForTheorem_6_8_fixed_or_fixed_eq_antipode_of_continuous_of_antipode_comp_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) ∨ ∃ (x : UnitSphereTwo), f x = helperForTheorem_6_8_antipode x

Helper for Theorem 6.8: any upstream principle asserting fixed-point-or-antipode- comp-fixed alternatives for continuous self-maps of S² yields the fixed-point-or- antipode-equality alternative.

theorem helperForTheorem_6_8_exists_fixed_or_antifixed_of_continuous_of_antipode_comp_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: any upstream principle asserting fixed-point-or-antipode- comp-fixed alternatives for continuous self-maps of S² yields the target fixed/anti- fixed alternative.

theorem helperForTheorem_6_8_fixed_or_fixed_eq_antipode_iff_exists_fixed_or_antifixed {f : UnitSphereTwo → UnitSphereTwo} : ((∃ (x : UnitSphereTwo), f x = x) ∨ ∃ (x : UnitSphereTwo), f x = helperForTheorem_6_8_antipode x) ↔ ∃ (x : UnitSphereTwo), f x = x ∨ ↑(f x) = -↑x

Helper for Theorem 6.8: the fixed-or-antipode-equality disjunction is equivalent to the target fixed/anti-fixed existence statement.

theorem helperForTheorem_6_8_global_exists_fixed_or_antifixed_iff_global_fixed_or_fixed_eq_antipode : (∀ (g : UnitSphereTwo → UnitSphereTwo), Continuous g → ∃ (x : UnitSphereTwo), g x = x ∨ ↑(g x) = -↑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: global fixed/anti-fixed existence and global fixed-or-antipode- equality principles on S² are equivalent.

theorem helperForTheorem_6_8_global_fixed_or_fixed_eq_antipode_iff_global_fixed_or_antipode_comp_fixed : (∀ (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), helperForTheorem_6_8_antipode (g x) = x

Helper for Theorem 6.8: global fixed-or-antipode-equality and global fixed-or- antipode ∘ g-fixed principles on S² are equivalent.

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

Helper for Theorem 6.8: global fixed/anti-fixed existence and global fixed-or- antipode ∘ g-fixed principles on S² are equivalent.

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

Helper for Theorem 6.8: a global fixed/anti-fixed existence principle for continuous self-maps of S² yields the global fixed-point-or-antipode ∘ g-fixed disjunction principle.

theorem helperForTheorem_6_8_fixed_or_fixed_eq_antipode_of_continuous_of_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) ∨ ∃ (x : UnitSphereTwo), f x = helperForTheorem_6_8_antipode x

Helper for Theorem 6.8: any upstream fixed/anti-fixed existence principle for continuous self-maps of S² yields the fixed-point-or-antipode-equality disjunction.

theorem helperForTheorem_6_8_fixed_or_antipode_comp_fixed_of_continuous_of_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) ∨ ∃ (x : UnitSphereTwo), helperForTheorem_6_8_antipode (f x) = x

Helper for Theorem 6.8: any upstream fixed/anti-fixed existence principle for continuous self-maps of S² yields the fixed-point-or-antipode ∘ f-fixed disjunction.

theorem helperForTheorem_6_8_global_fixed_or_fixed_eq_antipode_of_global_exists_fixed_or_antifixed (hprinciple : ∀ (g : UnitSphereTwo → UnitSphereTwo), Continuous g → ∃ (x : UnitSphereTwo), g x = x ∨ ↑(g x) = -↑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: a global fixed/anti-fixed existence principle for continuous self-maps of S² yields the global fixed-point-or-antipode-equality disjunction principle.

theorem helperForTheorem_6_8_fixed_or_fixed_eq_antipode_of_continuous_of_global_principle (hprinciple : ∀ (g : UnitSphereTwo → UnitSphereTwo), Continuous g → (∃ (x : UnitSphereTwo), g x = x) ∨ ∃ (x : UnitSphereTwo), g x = helperForTheorem_6_8_antipode x) (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: applying a global fixed-point-or-antipode-equality disjunction principle gives the local fixed-point-or-antipode-equality conclusion.

theorem helperForTheorem_6_8_global_exists_fixed_or_antifixed_of_borsuk_ulam_pipeline (hborsukUlam : ∀ (g : UnitSphereTwo → EuclideanSpace ℝ (Fin 2)), Continuous g → ∃ (x : UnitSphereTwo), g x = g (-x)) (hreduction : (∀ (g : UnitSphereTwo → EuclideanSpace ℝ (Fin 2)), Continuous g → ∃ (x : UnitSphereTwo), g x = g (-x)) → ∀ (g : UnitSphereTwo → UnitSphereTwo), Continuous g → ∃ (x : UnitSphereTwo), g x = x ∨ ↑(g x) = -↑x) (g : UnitSphereTwo → UnitSphereTwo) : Continuous g → ∃ (x : UnitSphereTwo), g x = x ∨ ↑(g x) = -↑x

Helper for Theorem 6.8: a Borsuk-Ulam-style antipodal-equality principle on maps S² → ℝ², together with a reduction from that principle to self-maps of S², yields the global fixed/anti-fixed existence principle on S².

theorem helperForTheorem_6_8_fixed_or_fixed_eq_antipode_of_continuous_of_borsuk_ulam_pipeline (hborsukUlam : ∀ (g : UnitSphereTwo → EuclideanSpace ℝ (Fin 2)), Continuous g → ∃ (x : UnitSphereTwo), g x = g (-x)) (hreduction : (∀ (g : UnitSphereTwo → EuclideanSpace ℝ (Fin 2)), Continuous g → ∃ (x : UnitSphereTwo), g x = g (-x)) → ∀ (g : UnitSphereTwo → UnitSphereTwo), Continuous g → ∃ (x : UnitSphereTwo), g x = x ∨ ↑(g x) = -↑x) (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: a Borsuk-Ulam-to-self-map reduction pipeline implies the local fixed-point-or-antipode-equality disjunction for continuous self-maps of S².

theorem helperForTheorem_6_8_exists_fixed_or_antifixed_of_continuous_of_borsuk_ulam_pipeline (hborsukUlam : ∀ (g : UnitSphereTwo → EuclideanSpace ℝ (Fin 2)), Continuous g → ∃ (x : UnitSphereTwo), g x = g (-x)) (hreduction : (∀ (g : UnitSphereTwo → EuclideanSpace ℝ (Fin 2)), Continuous g → ∃ (x : UnitSphereTwo), g x = g (-x)) → ∀ (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 Borsuk-Ulam-to-self-map reduction pipeline implies the target fixed/anti-fixed alternative for each continuous self-map of S².

theorem helperForTheorem_6_8_one_lt_rank_ambient : 1 < Module.rank ℝ (EuclideanSpace ℝ (Fin 3))

Helper for Theorem 6.8: the ambient space ℝ^3 has real module rank greater than one.