Theorem 13 — two non-separable sets with a common element have a non-separable union

Proved

WhitneyMatroid.Components.union_nonSeparable_of_common

by mikedeng1 · 1 vote · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

connectivitymatroidsp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $M$ be a finite matroid on a ground set $E$ , and let $M_1, M_2\subseteq E$ be non-separable submatroids having a common element $e$ . Then their union

M_1 + M_2

is non-separable.

This is the gluing property that makes the maximal non-separable parts (components) of a matroid pairwise disjoint (Theorem 14).

Formalization Note $M_1$ and $M_2$ are subsets of the ground set of a fixed finite matroid, as in Whitney's proof; $+$ is set union.

Preamble

import Mathlib
import Definitions.Def_WhitneyMatroid_Components_IsSeparable

Formal statement

namespace WhitneyMatroid.Components

theorem union_nonSeparable_of_common {α : Type*} (M : Matroid α) [M.Finite]
    (M₁ M₂ : Set α) (e : α) (h₁ : IsNonSeparable M M₁) (h₂ : IsNonSeparable M M₂)
    (he₁ : e ∈ M₁) (he₂ : e ∈ M₂) :
    IsNonSeparable M (M₁ ∪ M₂) := by sorry

end WhitneyMatroid.Components

Source

Whitney, On the Abstract Properties of Linear Dependence, Amer. J. Math. 57 (1935), p. 519, Theorem 13

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph