BG-01 interval transport of flats and hyperplanes across contraction by a flat. These statements implement the background correspondence used in lem:separation.

theorem TutteFormalization.flat_sdiff_contract {α : Type u_1} {M : Matroid α} {F H : Set α} (hH : M.IsFlat H) (hFH : F ⊆ H) : (M.contract F).IsFlat (H \ F)

theorem TutteFormalization.flat_union_of_contract_flat {α : Type u_1} {M : Matroid α} {F G : Set α} (hF : M.IsFlat F) (hG : (M.contract F).IsFlat G) : M.IsFlat (G ∪ F)

theorem TutteFormalization.hyperplane_sdiff_contract {α : Type u_1} {M : Matroid α} [M.Finite] {F H : Set α} (hF : M.IsFlat F) (hH : IsHyperplane M H) (hFH : F ⊆ H) : IsHyperplane (M.contract F) (H \ F)

theorem TutteFormalization.hyperplane_union_of_contract {α : Type u_1} {M : Matroid α} [M.Finite] {F G : Set α} (hF : M.IsFlat F) (hG : IsHyperplane (M.contract F) G) : IsHyperplane M (G ∪ F)

theorem TutteFormalization.indecomposable_sdiff_contract_iff {α : Type u_1} {M : Matroid α} {F H : Set α} (hH : M.IsFlat H) (hFH : F ⊆ H) : Indecomposable (M.contract F) (H \ F) ↔ Indecomposable M H

theorem TutteFormalization.ground_indecomposable {α : Type u_1} (M : Matroid α) [M.Finite] : Indecomposable M M.E