Chapter 15, Theorem 1: pairwise unlinked round circles

Proved

BookSixth.round_circle_unlink

by xiangyazi24 · Sep 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

proofs-from-the-booksixth-edition

Any finite collection of disjoint geometric round circles in real three-space is an unlink if each pair is an unlink. Here unlink means that an ambient isotopy, continuous together with its inverse, carries the ordered components to separated standard unit circles. It does not mean arbitrary loops are unlinked merely because pairs are.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.round_circle_unlink {m : ℕ} (C : Fin m → Set Space3) (hround : ∀ i, RoundCircle (C i)) (hdisjoint : ∀ i j, i ≠ j → Disjoint (C i) (C j)) (hpairs : ∀ i j, i ≠ j → IsUnlink (![C i, C j] : Fin 2 → Set Space3)) :
    IsUnlink C := by sorry

Source

Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), Chapter 15, Theorem 1: pairwise unlinked round circles, p. 100. https://doi.org/10.1007/978-3-662-57265-8_15

View graph