Moving sofa: related mathematical developments

• Cap.Foundations.Development008.

Moving sofa: related mathematical developments

• Cap.Monotone.

Cap / Monotone

theorem MovingSofa.isCompact_sdiff_capNiche {ω : ℝ} (K : CapSpace ω) : IsCompact (↑↑K \ capNiche K)

Removing the niche from a cap leaves a compact set.

theorem MovingSofa.cap_isMonotoneCap_iff_niche_subset {ω : ℝ} (K : CapSpace ω) : (∃ (s₀ : Set Point), IsStandardPosition s₀ ω ∧ ↑↑K = capOfSofa (monotonization s₀ ω) ω) ↔ capNiche K ⊆ ↑↑K