def BorsukUlam.Sphere (n : ℕ) : Set (EuclideanSpace ℝ (Fin (n + 1)))

The unit n-sphere S^n = { x ∈ ℝ^{n+1} : ‖x‖ = 1 }, regarded as a subset of the Euclidean space EuclideanSpace ℝ (Fin (n + 1)).

theorem BorsukUlam.neg_mem_sphere {n : ℕ} {x : EuclideanSpace ℝ (Fin (n + 1))} (hx : x ∈ Sphere n) : -x ∈ Sphere n

The unit sphere is closed under negation: if x ∈ S^n, then −x ∈ S^n. This is used to make sense of the antipodal hypothesis in Borsuk–Ulam.

theorem BorsukUlam.borsuk_ulam (n : ℕ) (f : C(↑(Sphere n), EuclideanSpace ℝ (Fin n))) (hf : ∀ (x : ↑(Sphere n)), f x = -f ⟨-↑x, ⋯⟩) : ∃ (x : ↑(Sphere n)), f x = 0

The Borsuk–Ulam theorem: any continuous antipodal map f : S^n → ℝ^n (satisfying f(−x) = −f(x) for all x ∈ S^n) has a zero, i.e. there exists x ∈ S^n with f(x) = 0.