structure Matroid.IsMutualBasis {α : Type u_1} {ι : Type u_2} (M : Matroid α) (B : Set α) (Xs : ι → Set α) : Prop

An independent set is a mutual basis for an indexed set family if it contains a basis for each set in the family.

• indep : M.Indep B
• forall_isBasis (i : ι) : M.IsBasis (Xs i ∩ B) (Xs i)

theorem Matroid.isMutualBasis_iff {α : Type u_1} {ι : Type u_2} (M : Matroid α) (B : Set α) (Xs : ι → Set α) : M.IsMutualBasis B Xs ↔ M.Indep B ∧ ∀ (i : ι), M.IsBasis (Xs i ∩ B) (Xs i)

instance Matroid.instGroundedPred₂SetForallIsMutualBasis {ι : Type u_2} : GroundedPred₂ fun {α : Type u_4} => IsMutualBasis

instance Matroid.instInvariantFun₂SetForallIsMutualBasis {ι : Type u_2} : InvariantFun₂ (fun {α : Type u_4} => IsMutualBasis) fun {β : Type u_5} => IsMutualBasis

theorem Matroid.IsMutualBasis.isBasis_inter {α : Type u_1} {ι : Type u_2} {M : Matroid α} {B : Set α} {Xs : ι → Set α} (h : M.IsMutualBasis B Xs) (i : ι) : M.IsBasis (Xs i ∩ B) (Xs i)

theorem Matroid.IsMutualBasis.subset_closure_inter {α : Type u_1} {ι : Type u_2} {M : Matroid α} {B : Set α} {Xs : ι → Set α} (h : M.IsMutualBasis B Xs) (i : ι) : Xs i ⊆ M.closure (Xs i ∩ B)

theorem Matroid.IsMutualBasis.closure_inter_eq {α : Type u_1} {ι : Type u_2} {M : Matroid α} {B : Set α} {Xs : ι → Set α} (h : M.IsMutualBasis B Xs) (i : ι) : M.closure (Xs i ∩ B) = M.closure (Xs i)

theorem Matroid.IsMutualBasis.subset_ground {α : Type u_1} {ι : Type u_2} {M : Matroid α} {B : Set α} {Xs : ι → Set α} (h : M.IsMutualBasis B Xs) (i : ι) : Xs i ⊆ M.E

theorem Matroid.IsMutualBasis.subtype {α : Type u_1} {η : Type u_3} {M : Matroid α} {B : Set α} {Xs : η → Set α} (h : M.IsMutualBasis B Xs) (A : Set η) : M.IsMutualBasis B fun (i : ↑A) => Xs ↑i

@[simp]

theorem Matroid.isMutualBasis_pair_iff {α : Type u_1} {M : Matroid α} {B X Y : Set α} : (M.IsMutualBasis B fun (i : ↑{X, Y}) => ↑i) ↔ M.Indep B ∧ M.IsBasis (X ∩ B) X ∧ M.IsBasis (Y ∩ B) Y

theorem Matroid.IsMutualBasis.isBasis_iInter {α : Type u_1} {ι : Type u_2} {M : Matroid α} {B : Set α} {Xs : ι → Set α} [Nonempty ι] (h : M.IsMutualBasis B Xs) : M.IsBasis ((⋂ (i : ι), Xs i) ∩ B) (⋂ (i : ι), Xs i)

theorem Matroid.IsMutualBasis.isBasis_iUnion {α : Type u_1} {ι : Type u_2} {M : Matroid α} {B : Set α} {Xs : ι → Set α} (h : M.IsMutualBasis B Xs) : M.IsBasis ((⋃ (i : ι), Xs i) ∩ B) (⋃ (i : ι), Xs i)

theorem Matroid.Indep.isMutualBasis_self {α : Type u_1} {ι : Type u_2} {M : Matroid α} {Xs : ι → Set α} (h : M.Indep (⋃ (i : ι), Xs i)) : M.IsMutualBasis (⋃ (i : ι), Xs i) Xs

theorem Matroid.Indep.isMutualBasis_of_forall_subset_closure {α : Type u_1} {ι : Type u_2} {M : Matroid α} {B : Set α} {Xs : ι → Set α} (hB : M.Indep B) (h : ∀ (i : ι), Xs i ⊆ M.closure (Xs i ∩ B)) : M.IsMutualBasis B Xs

theorem Matroid.IsMutualBasis.isBasis_biInter {α : Type u_1} {η : Type u_3} {A : Set η} {M : Matroid α} {B : Set α} {Xs : η → Set α} (h : M.IsMutualBasis B Xs) (hA : A.Nonempty) : M.IsBasis ((⋂ i ∈ A, Xs i) ∩ B) (⋂ i ∈ A, Xs i)

theorem Matroid.IsMutualBasis.iInter_subset_ground {α : Type u_1} {ι : Type u_2} {M : Matroid α} {B : Set α} {Xs : ι → Set α} [Nonempty ι] (h : M.IsMutualBasis B Xs) : ⋂ (i : ι), Xs i ⊆ M.E

theorem Matroid.IsMutualBasis.biInter_subset_ground {α : Type u_1} {η : Type u_3} {A : Set η} {M : Matroid α} {B : Set α} {Xs : η → Set α} (h : M.IsMutualBasis B Xs) (hA : A.Nonempty) : ⋂ i ∈ A, Xs i ⊆ M.E

theorem Matroid.IsMutualBasis.isBasis_biUnion {α : Type u_1} {η : Type u_3} {M : Matroid α} {B : Set α} {Xs : η → Set α} (h : M.IsMutualBasis B Xs) (A : Set η) : M.IsBasis ((⋃ i ∈ A, Xs i) ∩ B) (⋃ i ∈ A, Xs i)

theorem Matroid.IsMutualBasis.isMutualBasis_of_forall_subset_subset_closure {α : Type u_1} {ι : Type u_2} {M : Matroid α} {B : Set α} {Xs Ys : ι → Set α} (hB : M.IsMutualBasis B Xs) (hXY : ∀ (i : ι), Xs i ⊆ Ys i) (hYX : ∀ (i : ι), Ys i ⊆ M.closure (Xs i)) : M.IsMutualBasis B Ys

theorem Matroid.IsMutualBasis.isMutualBasis_cls {α : Type u_1} {ι : Type u_2} {M : Matroid α} {B : Set α} {Xs : ι → Set α} (hB : M.IsMutualBasis B Xs) : M.IsMutualBasis B fun (i : ι) => M.closure (Xs i)

theorem Matroid.IsMutualBasis.iInter_closure_eq_closure_iInter {α : Type u_1} {ι : Type u_2} {M : Matroid α} {B : Set α} {Xs : ι → Set α} [Nonempty ι] (hB : M.IsMutualBasis B Xs) : ⋂ (i : ι), M.closure (Xs i) = M.closure (⋂ (i : ι), Xs i)

theorem Matroid.Indep.isMutualBasis_powerset {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.Indep B) : M.IsMutualBasis B fun (I : ↑(𝒫 B)) => ↑I

theorem Matroid.IsMutualBasis.switch {α : Type u_1} {ι : Type u_2} {M : Matroid α} {B I : Set α} {Xs : ι → Set α} (hB : M.IsMutualBasis B Xs) (hIX : M.IsBasis I (⋂ (i : ι), Xs i)) : M.IsMutualBasis ((B \ ⋂ (i : ι), Xs i) ∪ I) Xs

Given a mutual basis B for Xs, we can switch out the intersection of B with the intersection of the Xs with any other base for the intersection of the Xs and still have a mutual basis.

theorem Matroid.IsMutualBasis.comp {α : Type u_1} {ι : Type u_2} {M : Matroid α} {B : Set α} {ζ : Type u_4} {Xs : ι → Set α} (h : M.IsMutualBasis B Xs) (t : ζ → ι) : M.IsMutualBasis B (Xs ∘ t)

theorem Matroid.IsMutualBasis.mono {α : Type u_1} {ι : Type u_2} {M : Matroid α} {B I : Set α} {Xs : ι → Set α} (hI : M.IsMutualBasis I Xs) (hIB : I ⊆ B) (hB : M.Indep B) : M.IsMutualBasis B Xs

theorem Matroid.IsMutualBasis.isMutualBasis_compl_dual {α : Type u_1} {ι : Type u_2} {M : Matroid α} {B : Set α} {Xs : ι → Set α} (h : M.IsMutualBasis B Xs) (hB : M.IsBase B) : M✶.IsMutualBasis (M.E \ B) fun (i : ι) => M.E \ Xs i

theorem Matroid.IsMutualBasis.isMutualBasis_compl_ofDual {α : Type u_1} {ι : Type u_2} {M : Matroid α} {B : Set α} {Xs : ι → Set α} (h : M✶.IsMutualBasis B Xs) (hB : M✶.IsBase B) : M.IsMutualBasis (M.E \ B) fun (i : ι) => M.E \ Xs i

theorem Matroid.IsMutualBasis.isMutualBasis_of_compl {α : Type u_1} {ι : Type u_2} {M : Matroid α} {B : Set α} {Xs : ι → Set α} (hXs : ∀ (i : ι), Xs i ⊆ M.E) (h : M.IsMutualBasis B fun (i : ι) => M.E \ Xs i) (hB : M.IsBase B) : M✶.IsMutualBasis (M.E \ B) Xs

def Matroid.IsModularFamily {α : Type u_1} {ι : Type u_2} (M : Matroid α) (Xs : ι → Set α) : Prop

A set family is a IsModularFamily if it has a modular base.

Equations

• M.IsModularFamily Xs = ∃ (B : Set α), M.IsMutualBasis B Xs

instance Matroid.instGroundedPredForallSetIsModularFamily {ι : Type u_2} : GroundedPred fun {α : Type u_4} => IsModularFamily

instance Matroid.instInvariantFunForallSetPropIsModularFamily {ι : Type u_2} : InvariantFun (fun {α : Type u_4} => IsModularFamily) fun {β : Type u_5} => IsModularFamily

theorem Matroid.Indep.isModularFamily {α : Type u_1} {ι : Type u_2} {M : Matroid α} {I : Set α} {Xs : ι → Set α} (hI : M.Indep I) (hXs : ∀ (i : ι), M.IsBasis (Xs i ∩ I) (Xs i)) : M.IsModularFamily Xs

theorem Matroid.IsModularFamily.exists_isMutualBasis_isBase {α : Type u_1} {ι : Type u_2} {M : Matroid α} {Xs : ι → Set α} (h : M.IsModularFamily Xs) : ∃ (B : Set α), M.IsBase B ∧ M.IsMutualBasis B Xs

theorem Matroid.IsMutualBasis.isModularFamily {α : Type u_1} {ι : Type u_2} {M : Matroid α} {B : Set α} {Xs : ι → Set α} (hB : M.IsMutualBasis B Xs) : M.IsModularFamily Xs

theorem Matroid.IsModularFamily.subset_ground_of_mem {α : Type u_1} {ι : Type u_2} {M : Matroid α} {Xs : ι → Set α} (h : M.IsModularFamily Xs) (i : ι) : Xs i ⊆ M.E

theorem Matroid.IsModularFamily.iInter_closure_eq_closure_iInter {α : Type u_1} {ι : Type u_2} {M : Matroid α} {Xs : ι → Set α} [Nonempty ι] (hXs : M.IsModularFamily Xs) : ⋂ (i : ι), M.closure (Xs i) = M.closure (⋂ (i : ι), Xs i)

theorem Matroid.Indep.isModularFamily_of_subsets {α : Type u_1} {ι : Type u_2} {M : Matroid α} {I : Set α} {Js : ι → Set α} (hI : M.Indep I) (hJs : ⋃ (i : ι), Js i ⊆ I) : M.IsModularFamily Js

theorem Matroid.IsModularFamily.isModularFamily_of_forall_subset_closure {α : Type u_1} {ι : Type u_2} {M : Matroid α} {Xs Ys : ι → Set α} (h : M.IsModularFamily Xs) (hXY : ∀ (i : ι), Xs i ⊆ Ys i) (hYX : ∀ (i : ι), Ys i ⊆ M.closure (Xs i)) : M.IsModularFamily Ys

theorem Matroid.IsModularFamily.cls_isModularFamily {α : Type u_1} {ι : Type u_2} {M : Matroid α} {Xs : ι → Set α} (h : M.IsModularFamily Xs) : M.IsModularFamily fun (i : ι) => M.closure (Xs i)

@[simp]

theorem Matroid.isModularFamily_of_isEmpty {α : Type u_1} {ι : Type u_2} {M : Matroid α} {Xs : ι → Set α} [IsEmpty ι] : M.IsModularFamily Xs

@[simp]

theorem Matroid.isModularFamily_iff_of_subsingleton {α : Type u_1} {ι : Type u_2} {M : Matroid α} {Xs : ι → Set α} [Subsingleton ι] : M.IsModularFamily Xs ↔ ∀ (i : ι), Xs i ⊆ M.E

theorem Matroid.isModularFamily_of_isLoopEquiv {α : Type u_1} {ι : Type u_2} {M : Matroid α} {Xs Ys : ι → Set α} (h : M.IsModularFamily Xs) (he : ∀ (i : ι), M.IsLoopEquiv (Xs i) (Ys i)) : M.IsModularFamily Ys

theorem Matroid.IsModularFamily.restrict {α : Type u_1} {ι : Type u_2} {M : Matroid α} {Xs : ι → Set α} {R : Set α} (h : M.IsModularFamily Xs) (hXR : ∀ (i : ι), Xs i ⊆ R) : (M.restrict R).IsModularFamily Xs

theorem Matroid.IsModularFamily.delete {α : Type u_1} {ι : Type u_2} {M : Matroid α} {Xs : ι → Set α} {D : Set α} (h : M.IsModularFamily Xs) (hXD : ∀ (i : ι), Disjoint (Xs i) D) : (M.delete D).IsModularFamily Xs

theorem Matroid.IsModularFamily.ofRestrict' {α : Type u_1} {ι : Type u_2} {M : Matroid α} {Xs : ι → Set α} {R : Set α} (h : (M.restrict R).IsModularFamily Xs) : M.IsModularFamily fun (i : ι) => Xs i ∩ M.E

theorem Matroid.IsModularFamily.ofRestrict {α : Type u_1} {ι : Type u_2} {Xs : ι → Set α} {M : Matroid α} {R : Set α} (hR : R ⊆ M.E) (h : (M.restrict R).IsModularFamily Xs) : M.IsModularFamily Xs

theorem Matroid.IsModularFamily.comp {α : Type u_1} {ι : Type u_2} {M : Matroid α} {Xs : ι → Set α} {ζ : Type u_4} (h : M.IsModularFamily Xs) (t : ζ → ι) : M.IsModularFamily (Xs ∘ t)

A subfamily of a modular family is a modular family.

theorem Matroid.IsModularFamily.set_biInter_comp {α : Type u_1} {ι : Type u_2} {η : Type u_3} {M : Matroid α} {Xs : η → Set α} (h : M.IsModularFamily Xs) (t : ι → Set η) (ht : ∀ (j : ι), (t j).Nonempty) : M.IsModularFamily fun (j : ι) => ⋂ i ∈ t j, Xs i

theorem Matroid.IsModularFamily.map {α : Type u_1} {ι : Type u_2} {M : Matroid α} {Xs : ι → Set α} {β : Type u_4} (f : α → β) (hf : Set.InjOn f M.E) (h : M.IsModularFamily Xs) : (M.map f hf).IsModularFamily fun (i : ι) => f '' Xs i

theorem Matroid.IsModularFamily.of_comap {α : Type u_1} {ι : Type u_2} {Xs : ι → Set α} {β : Type u_4} {f : α → β} {M : Matroid β} (hX : (M.comap f).IsModularFamily Xs) : M.IsModularFamily fun (i : ι) => f '' Xs i

theorem Matroid.IsModularFamily.comap_iff {α : Type u_1} {ι : Type u_2} {Xs : ι → Set α} {β : Type u_4} {f : α → β} {M : Matroid β} (hf : Function.Injective f) : (M.comap f).IsModularFamily Xs ↔ M.IsModularFamily fun (i : ι) => f '' Xs i

theorem Matroid.isModularFamily_map_iff {α : Type u_1} {ι : Type u_2} {η : Type u_3} {M : Matroid α} (f : α → η) (hf : Set.InjOn f M.E) {Xs : ι → Set η} : (M.map f hf).IsModularFamily Xs ↔ ∃ (Ys : ι → Set α), M.IsModularFamily Ys ∧ ∀ (i : ι), Xs i = f '' Ys i

theorem Matroid.IsModularFamily.mapEmbedding {α : Type u_1} {ι : Type u_2} {M : Matroid α} {Xs : ι → Set α} {β : Type u_4} (f : α ↪ β) (h : M.IsModularFamily Xs) : (M.mapEmbedding f).IsModularFamily fun (i : ι) => ⇑f '' Xs i

theorem Matroid.IsModularFamily.of_contract_indep {α : Type u_1} {ι : Type u_2} {M : Matroid α} {I : Set α} {Xs : ι → Set α} (h : (M.contract I).IsModularFamily Xs) (hI : M.Indep I) : M.IsModularFamily fun (i : ι) => Xs i ∪ I

theorem Matroid.IsModularFamily.exists_isMutualBasis_superset_of_indep_of_subset_inter {α : Type u_1} {ι : Type u_2} {M : Matroid α} {I : Set α} {Xs : ι → Set α} (h : M.IsModularFamily Xs) (hI : M.Indep I) (hIX : I ⊆ ⋂ (i : ι), Xs i) : ∃ (B : Set α), M.IsMutualBasis B Xs ∧ I ⊆ B

A mutual basis can be chosen to contain a prescribed independent subset of the intersection.

theorem Matroid.IsModularFamily.contract {α : Type u_1} {ι : Type u_2} {M : Matroid α} {Xs : ι → Set α} (h : M.IsModularFamily Xs) {C : Set α} (hC : ∀ (i : ι), C ⊆ M.closure (Xs i)) : (M.contract C).IsModularFamily fun (i : ι) => Xs i \ C

If C is spanned by the intersection of a modular family Xs, then we get a modular family in M ／ C. TODO : Is this true for all C ⊆ ⋃ i, X i?

theorem Matroid.IsModularFamily.of_project {α : Type u_1} {ι : Type u_2} {M : Matroid α} {Xs : ι → Set α} {C : Set α} (h : (M.project C).IsModularFamily Xs) (hCX : ∀ (i : ι), C ⊆ Xs i) : M.IsModularFamily Xs

theorem Matroid.IsModularFamily.finite_of_forall_isFlat {α : Type u_1} {ι : Type u_2} {M : Matroid α} {Xs : ι → Set α} [M.RankFinite] (h : M.IsModularFamily Xs) (h_isFlat : ∀ (i : ι), M.IsFlat (Xs i)) : (Set.range Xs).Finite

A IsModularFamily of flats in a finite-rank matroid is finite.

theorem Matroid.isModularFamily_disjointSigma_iff {α : Type u_1} {ι : Type u_2} {η : Type u_3} (Xs : ι → Set α) {M : η → Matroid α} {hdj : Pairwise (Function.onFun Disjoint fun (i : η) => (M i).E)} : (Matroid.disjointSigma M hdj).IsModularFamily Xs ↔ (∀ (c : η), (M c).IsModularFamily fun (i : ι) => Xs i ∩ (M c).E) ∧ ∀ (i : ι), Xs i ⊆ ⋃ (c : η), (M c).E

theorem Matroid.isModularFamily_disjointSum_iff {α : Type u_1} {ι : Type u_2} {Xs : ι → Set α} {M N : Matroid α} (hdj : Disjoint M.E N.E) : (M.disjointSum N hdj).IsModularFamily Xs ↔ (M.IsModularFamily fun (i : ι) => Xs i ∩ M.E) ∧ (N.IsModularFamily fun (i : ι) => Xs i ∩ N.E) ∧ ∀ (i : ι), Xs i ⊆ M.E ∪ N.E

def Matroid.IsModularPair {α : Type u_1} (M : Matroid α) (X Y : Set α) : Prop

Sets X,Y are a modular pair if some independent set contains bases for both.

Equations

• M.IsModularPair X Y = M.IsModularFamily fun (i : Bool) => bif i then X else Y

theorem Matroid.IsModularPair.symm {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsModularPair X Y) : M.IsModularPair Y X

theorem Matroid.isModularPair_comm {α : Type u_1} {M : Matroid α} {X Y : Set α} : M.IsModularPair X Y ↔ M.IsModularPair Y X

theorem Matroid.IsModularPair.subset_ground_left {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsModularPair X Y) : X ⊆ M.E

theorem Matroid.IsModularPair.subset_ground_right {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsModularPair X Y) : Y ⊆ M.E

theorem Matroid.isModularPair_iff {α : Type u_1} {M : Matroid α} {X Y : Set α} : M.IsModularPair X Y ↔ ∃ (I : Set α), M.Indep I ∧ M.IsBasis (X ∩ I) X ∧ M.IsBasis (Y ∩ I) Y

theorem Matroid.IsModularFamily.isModularPair {α : Type u_1} {ι : Type u_2} {M : Matroid α} {Xs : ι → Set α} (h : M.IsModularFamily Xs) (i j : ι) : M.IsModularPair (Xs i) (Xs j)

theorem Matroid.isModularPair_iff_exists_subsets_closure_inter {α : Type u_1} {M : Matroid α} {X Y : Set α} : M.IsModularPair X Y ↔ ∃ (I : Set α), M.Indep I ∧ X ⊆ M.closure (X ∩ I) ∧ Y ⊆ M.closure (Y ∩ I)

theorem Matroid.IsModularPair.exists_subsets_closure_inter {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsModularPair X Y) : ∃ (I : Set α), M.Indep I ∧ X ⊆ M.closure (X ∩ I) ∧ Y ⊆ M.closure (Y ∩ I)

theorem Matroid.isModularPair_iff_exists_isBasis_isBasis {α : Type u_1} {M : Matroid α} {X Y : Set α} : M.IsModularPair X Y ↔ ∃ (I : Set α) (J : Set α), M.IsBasis I X ∧ M.IsBasis J Y ∧ M.Indep (I ∪ J)

theorem Matroid.IsModularPair.exists_isMutualBasis_isBase {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsModularPair X Y) : ∃ (B : Set α), M.IsBase B ∧ M.IsBasis ((X ∪ Y) ∩ B) (X ∪ Y) ∧ M.IsBasis (X ∩ B) X ∧ M.IsBasis (Y ∩ B) Y ∧ M.IsBasis (X ∩ Y ∩ B) (X ∩ Y)

theorem Matroid.IsModularPair.exists_common_isBasis {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsModularPair X Y) : ∃ (I : Set α), M.IsBasis I (X ∪ Y) ∧ M.IsBasis (I ∩ X) X ∧ M.IsBasis (I ∩ Y) Y ∧ M.IsBasis (I ∩ X ∩ Y) (X ∩ Y)

theorem Matroid.IsModularPair.inter_closure_eq {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsModularPair X Y) : M.closure (X ∩ Y) = M.closure X ∩ M.closure Y

theorem Matroid.isModularPair_of_subset {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXY : X ⊆ Y) (hY : Y ⊆ M.E) : M.IsModularPair X Y

theorem Matroid.Indep.isModularPair_of_union {α : Type u_1} {M : Matroid α} {I J : Set α} (hi : M.Indep (I ∪ J)) : M.IsModularPair I J

theorem Matroid.IsModularPair.of_subset_closure_subset_closure {α : Type u_1} {M : Matroid α} {X X' Y Y' : Set α} (h : M.IsModularPair X Y) (hXX' : X ⊆ X') (hX' : X' ⊆ M.closure X) (hYY' : Y ⊆ Y') (hY' : Y' ⊆ M.closure Y) : M.IsModularPair X' Y'

theorem Matroid.IsModularPair.of_subset_closure_left {α : Type u_1} {M : Matroid α} {X X' Y : Set α} (h : M.IsModularPair X Y) (hXX' : X ⊆ X') (hX' : X' ⊆ M.closure X) : M.IsModularPair X' Y

theorem Matroid.IsModularPair.of_subset_closure_right {α : Type u_1} {M : Matroid α} {X Y Y' : Set α} (h : M.IsModularPair X Y) (hYY' : Y ⊆ Y') (hY' : Y' ⊆ M.closure Y) : M.IsModularPair X Y'

theorem Matroid.IsModularPair.of_isBasis_left {α : Type u_1} {M : Matroid α} {I X Y : Set α} (h : M.IsModularPair I Y) (hIX : M.IsBasis I X) : M.IsModularPair X Y

theorem Matroid.IsModularPair.of_isBasis_right {α : Type u_1} {M : Matroid α} {J X Y : Set α} (h : M.IsModularPair X J) (hJY : M.IsBasis J Y) : M.IsModularPair X Y

theorem Matroid.IsModularPair.of_isBasis_of_isBasis {α : Type u_1} {M : Matroid α} {I J X Y : Set α} (h : M.IsModularPair I J) (hIX : M.IsBasis I X) (hJY : M.IsBasis J Y) : M.IsModularPair X Y

theorem Matroid.IsModularPair.closure_left {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsModularPair X Y) : M.IsModularPair (M.closure X) Y

theorem Matroid.IsModularPair.closure_right {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsModularPair X Y) : M.IsModularPair X (M.closure Y)

theorem Matroid.IsModularPair.closure_closure {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsModularPair X Y) : M.IsModularPair (M.closure X) (M.closure Y)

theorem Matroid.isModularPair_loops {α : Type u_1} {X : Set α} (M : Matroid α) (hX : X ⊆ M.E) : M.IsModularPair X M.loops

theorem Matroid.Spanning.isModularPair_iff {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : M.Spanning X) : M.IsModularPair X Y ↔ Y ⊆ M.closure (X ∩ Y)

theorem Matroid.isModularPair_singleton {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ M.E) (hX : X ⊆ M.E) (heX : e ∉ M.closure X) : M.IsModularPair {e} X

theorem Matroid.IsModularPair.eRk_add_eRk {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsModularPair X Y) : M.eRk X + M.eRk Y = M.eRk (X ∩ Y) + M.eRk (X ∪ Y)

theorem Matroid.IsRkFinite.isModularPair_iff_eRk {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXfin : M.IsRkFinite X) (hYfin : M.IsRkFinite Y) (hXE : X ⊆ M.E := by aesop_mat) (hYE : Y ⊆ M.E := by aesop_mat) : M.IsModularPair X Y ↔ M.eRk X + M.eRk Y = M.eRk (X ∩ Y) + M.eRk (X ∪ Y)

theorem Matroid.IsRkFinite.isModularPair_iff_rk {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXfin : M.IsRkFinite X) (hYfin : M.IsRkFinite Y) (hXE : X ⊆ M.E := by aesop_mat) (hYE : Y ⊆ M.E := by aesop_mat) : M.IsModularPair X Y ↔ M.rk X + M.rk Y = M.rk (X ∩ Y) + M.rk (X ∪ Y)

theorem Matroid.isModularPair_iff_rk {α : Type u_1} {M : Matroid α} {X Y : Set α} [M.RankFinite] (hXE : X ⊆ M.E := by aesop_mat) (hYE : Y ⊆ M.E := by aesop_mat) : M.IsModularPair X Y ↔ M.rk X + M.rk Y = M.rk (X ∩ Y) + M.rk (X ∪ Y)

theorem Matroid.IsModularFamily.isModularPair_compl_biUnion {α : Type u_1} {η : Type u_3} {M : Matroid α} {Xs : η → Set α} (h : M.IsModularFamily Xs) (A : Set η) : M.IsModularPair (⋃ i ∈ A, Xs i) (⋃ i ∈ Aᶜ, Xs i)

theorem Matroid.IsModularFamily.isModularPair_compl_biInter {α : Type u_1} {η : Type u_3} {M : Matroid α} {Xs : η → Set α} (h : M.IsModularFamily Xs) (A : Set η) (hA : A.Nonempty) (hA' : A ≠ Set.univ) : M.IsModularPair (⋂ i ∈ A, Xs i) (⋂ i ∈ Aᶜ, Xs i)

theorem Matroid.IsModularFamily.isModularPair_singleton_compl_biUnion {α : Type u_1} {η : Type u_3} {M : Matroid α} {Xs : η → Set α} (h : M.IsModularFamily Xs) (i₀ : η) : M.IsModularPair (Xs i₀) (⋃ i ∈ {i₀}ᶜ, Xs i)

theorem Matroid.IsModularFamily.isModularPair_singleton_compl_biInter {α : Type u_1} {η : Type u_3} {M : Matroid α} [Nontrivial η] {Xs : η → Set α} (h : M.IsModularFamily Xs) (i₀ : η) : M.IsModularPair (Xs i₀) (⋂ i ∈ {i₀}ᶜ, Xs i)

theorem Matroid.isModularPair_insert_closure {α : Type u_1} (M : Matroid α) (X : Set α) (e f : α) : M.IsModularPair (M.closure (insert e X)) (M.closure (insert f X))

theorem Matroid.IsModularPair.restrict {α : Type u_1} {M : Matroid α} {X Y R : Set α} (hXY : M.IsModularPair X Y) (hXR : X ⊆ R) (hYR : Y ⊆ R) : (M.restrict R).IsModularPair X Y

theorem Matroid.IsModularPair.contract_subset_closure {α : Type u_1} {M : Matroid α} {X Y C : Set α} (hXY : M.IsModularPair X Y) (hCX : C ⊆ M.closure X) (hCY : C ⊆ M.closure Y) : (M.contract C).IsModularPair (X \ C) (Y \ C)

theorem Matroid.Coindep.subset_closure_iff_isModularPair {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : M.Coindep (X \ Y)) (hY : Y ⊆ M.E := by aesop_mat) : X ⊆ M.closure Y ↔ M.IsModularPair (X ∪ Y) (M.E \ (X \ Y))

theorem Matroid.isModularPair_disjointSigma_iff {α : Type u_1} {η : Type u_3} (X Y : Set α) {M : η → Matroid α} {hdj : Pairwise (Function.onFun Disjoint fun (i : η) => (M i).E)} : (Matroid.disjointSigma M hdj).IsModularPair X Y ↔ (∀ (c : η), (M c).IsModularPair (X ∩ (M c).E) (Y ∩ (M c).E)) ∧ X ∪ Y ⊆ ⋃ (c : η), (M c).E

theorem Matroid.isModularPair_disjointSum_iff {α : Type u_1} (X Y : Set α) {M N : Matroid α} {hdj : Disjoint M.E N.E} : (M.disjointSum N hdj).IsModularPair X Y ↔ M.IsModularPair (X ∩ M.E) (Y ∩ M.E) ∧ N.IsModularPair (X ∩ N.E) (Y ∩ N.E) ∧ X ∪ Y ⊆ M.E ∪ N.E