Theorem 14 — distinct components are disjoint
ProvedWhitneyMatroid.Components.components_disjointconnectivitymatroidsp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1
Let be a finite matroid. If and are components of (maximal nonempty non-separable subsets of the ground set) and , then
That is, no two distinct components of have common elements.
Formalization Note Components are those of the definition IsComponent (rank-defined, nonempty).
Preamble
import Mathlib import Definitions.Def_WhitneyMatroid_Components_IsSeparable import Definitions.Def_WhitneyMatroid_Components_IsComponent
Formal statement
namespace WhitneyMatroid.Components
theorem components_disjoint {α : Type*} (M : Matroid α) [M.Finite]
(K₁ K₂ : Set α) (hK₁ : IsComponent M K₁) (hK₂ : IsComponent M K₂) (hne : K₁ ≠ K₂) :
Disjoint K₁ K₂ := by sorry
end WhitneyMatroid.Components
Source
Whitney, On the Abstract Properties of Linear Dependence, Amer. J. Math. 57 (1935), p. 519, Theorem 14
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.