Bing's house with two rooms

DefinitionBing's house with two rooms#✓fully proved

Bing's house with two rooms, in the version drawn in Hatcher's Algebraic Topology, is the subset \(H\) of \(\mathbb{R} \times \mathbb{R} \times \mathbb{R}\) consisting of the points of \([0,4] \times [0,3] \times \{0,1,2\}\) that lie in none of \((2,3) \times (1,2) \times \{0\}\), \((1,3) \times (1,2) \times \{1\}\) and \((1,2) \times (1,2) \times \{2\}\) (three floors with holes), together with the inner walls \(\{1\} \times [1,2] \times [1,2]\), \(\{2\} \times [1,3] \times [0,2]\), \(\{3\} \times [1,2] \times [0,1]\), \([1,2] \times \{1,2\} \times [1,2]\) and \([2,3] \times \{1,2\} \times [0,1]\), and the outer walls \([0,4] \times \{0,3\} \times [0,2]\) and \(\{0,4\} \times [0,3] \times [0,2]\).

def HouseWithTwoRooms : Set (ℝ × ℝ × ℝ) :=
  (Icc 0 4 ×ˢ Icc 0 3 ×ˢ {0, 1, 2} \
    (Ioo 2 3 ×ˢ Ioo 1 2 ×ˢ {0} ∪ Ioo 1 3 ×ˢ Ioo 1 2 ×ˢ {1} ∪ Ioo 1 2 ×ˢ Ioo 1 2 ×ˢ {2})) ∪
  ({1} ×ˢ Icc 1 2 ×ˢ Icc 1 2 ∪ {2} ×ˢ Icc 1 3 ×ˢ Icc 0 2 ∪ {3} ×ˢ Icc 1 2 ×ˢ Icc 0 1 ∪
    Icc 1 2 ×ˢ {1, 2} ×ˢ Icc 1 2 ∪ Icc 2 3 ×ˢ {1, 2} ×ˢ Icc 0 1) ∪
  (Icc 0 4 ×ˢ {0, 3} ×ˢ Icc 0 2 ∪ {0, 4} ×ˢ Icc 0 3 ×ˢ Icc 0 2)

Used by 1

Used byBing's house with two rooms is contractible

TheoremBing's house with two rooms is contractible#●ready to prove

Bing's house with two rooms, regarded as a subspace of \(\mathbb{R} \times \mathbb{R} \times \mathbb{R}\), is contractible.

public theorem_wanted contractibleSpace_houseWithTwoRooms : ContractibleSpace HouseWithTwoRooms

Sources

• Allen Hatcher, Algebraic Topology. Problem contractibleSpace_houseWithTwoRooms of the lean-eval benchmark.

Uses 1

Statement usesBing's house with two rooms

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.