Bing's house with two rooms is contractible | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: Allen Hatcher, *Algebraic Topology*.

Informal solution: Show that a neighborhood of the space deformation retracts onto it and is homeomorphic to a 3-ball.

theorem declaration uses `sorry`contractibleSpace_houseWithTwoRooms : ContractibleSpace LeanEval.Topology.HouseWithTwoRooms := by⊢ ContractibleSpace ↑HouseWithTwoRooms
  sorryAll goals completed! 🐙