Chapter 15 bridge: the empty family is an unlink
ProvedBookSixth.round_circle_unlink_emptyproofs-from-the-bookround-circlessixth-edition
The empty ordered family of components is an unlink. This is the base case for the finite round-circle induction in Chapter 15, Theorem 1.
Preamble
import Mathlib import Definitions.Def_BookSixth open scoped BigOperators open BookSixth
Formal statement
theorem BookSixth.round_circle_unlink_empty : IsUnlink (fun _ : Fin 0 => (∅ : Set Space3)) := by sorry
Source
Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), Chapter 15, Theorem 1, p. 100. Base-case adapter for BookSixth.round_circle_unlink. https://doi.org/10.1007/978-3-662-57265-8_15