structure Matroid.IsSkewFamily {α : Type u_1} {ι : Type u_3} (M : Matroid α) (Xs : ι → Set α) : Prop

A SkewFamily in a matroid is a collection of sets having pairwise disjoint bases whose union is independent.

• isModularFamily : M.IsModularFamily Xs
• disj ⦃i j : ι⦄ : i ≠ j → Xs i ∩ Xs j ⊆ M.loops

theorem Matroid.isSkewFamily_iff {α : Type u_1} {ι : Type u_3} (M : Matroid α) (Xs : ι → Set α) : M.IsSkewFamily Xs ↔ M.IsModularFamily Xs ∧ ∀ ⦃i j : ι⦄, i ≠ j → Xs i ∩ Xs j ⊆ M.loops

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

theorem Matroid.IsSkewFamily.isLoop_of_mem_inter {α : Type u_1} {ι : Type u_3} {M : Matroid α} {e : α} {Xs : ι → Set α} {i j : ι} (h : M.IsSkewFamily Xs) (hij : i ≠ j) (he : e ∈ Xs i ∩ Xs j) : M.IsLoop e

theorem Matroid.IsSkewFamily.subset_loops_of_ne {α : Type u_1} {ι : Type u_3} {M : Matroid α} {Xs : ι → Set α} {i j : ι} (h : M.IsSkewFamily Xs) (hij : i ≠ j) : Xs i ∩ Xs j ⊆ M.loops

theorem Matroid.IsSkewFamily.pairwise_subset_loops {α : Type u_1} {η : Type u_2} {M : Matroid α} {Xs : η → Set α} (h : M.IsSkewFamily Xs) : Pairwise fun (i j : η) => Xs i ∩ Xs j ⊆ M.loops

theorem Matroid.IsSkewFamily.comp {α : Type u_1} {ι : Type u_3} {M : Matroid α} {Xs : ι → Set α} {ζ : Type u_4} (h : M.IsSkewFamily Xs) (t : ζ → ι) (ht : Function.Injective t) : M.IsSkewFamily (Xs ∘ t)

@[simp]

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

theorem Matroid.IsSkewFamily.disjoint_inter_indep {α : Type u_1} {ι : Type u_3} {M : Matroid α} {Xs : ι → Set α} {i j : ι} {I : Set α} (h : M.IsSkewFamily Xs) (hI : M.Indep I) (hij : i ≠ j) : Disjoint (Xs i ∩ I) (Xs j)

theorem Matroid.IsSkewFamily.diff_loops_pairwise_disjoint {α : Type u_1} {η : Type u_2} {M : Matroid α} {Xs : η → Set α} (h : M.IsSkewFamily Xs) : Pairwise (Function.onFun Disjoint fun (i : η) => Xs i \ M.loops)

theorem Matroid.IsSkewFamily.disjoint_of_indep_subset {α : Type u_1} {ι : Type u_3} {M : Matroid α} {Xs : ι → Set α} {i j : ι} {I : Set α} (h : M.IsSkewFamily Xs) (hI : M.Indep I) (hIX : I ⊆ Xs i) (hij : i ≠ j) : Disjoint I (Xs j)

theorem Matroid.IsSkewFamily.pairwise_disjoint_inter_of_indep {α : Type u_1} {η : Type u_2} {M : Matroid α} {I : Set α} {Xs : η → Set α} (h : M.IsSkewFamily Xs) (hI : M.Indep I) : Pairwise (Function.onFun Disjoint fun (i : η) => Xs i ∩ I)

theorem Matroid.IsSkewFamily.pairwise_disjoint_of_indep_subsets {α : Type u_1} {η : Type u_2} {M : Matroid α} {Is Xs : η → Set α} (h : M.IsSkewFamily Xs) (hIX : ∀ (i : η), Is i ⊆ Xs i) (hIs : ∀ (i : η), M.Indep (Is i)) : Pairwise (Function.onFun Disjoint Is)

theorem Matroid.IsSkewFamily.pairwise_disjoint_of_isBases {α : Type u_1} {η : Type u_2} {M : Matroid α} {Is Xs : η → Set α} (h : M.IsSkewFamily Xs) (hIX : ∀ (i : η), M.IsBasis (Is i) (Xs i)) : Pairwise (Function.onFun Disjoint Is)

theorem Matroid.IsSkewFamily.cls_isSkewFamily {α : Type u_1} {ι : Type u_3} {M : Matroid α} {Xs : ι → Set α} (h : M.IsSkewFamily Xs) : M.IsSkewFamily fun (i : ι) => M.closure (Xs i)

theorem Matroid.Indep.isSkewFamily_of_disjoint_isBases {α : Type u_1} {η : Type u_2} {M : Matroid α} {Is Xs : η → Set α} (hI : M.Indep (⋃ (i : η), Is i)) (hdj : Pairwise (Function.onFun Disjoint Is)) (hIs : ∀ (i : η), M.IsBasis (Is i) (Xs i)) : M.IsSkewFamily Xs

theorem Matroid.isSkewFamily_iff_exist_isBases {α : Type u_1} {η : Type u_2} {M : Matroid α} {Xs : η → Set α} : M.IsSkewFamily Xs ↔ ∃ (Is : η → Set α), Pairwise (Function.onFun Disjoint Is) ∧ M.IsBasis (⋃ (i : η), Is i) (⋃ (i : η), Xs i) ∧ ∀ (i : η), M.IsBasis (Is i) (Xs i)

theorem Matroid.IsSkewFamily.restrict {α : Type u_1} {η : Type u_2} {M : Matroid α} {Xs : η → Set α} {R : Set α} (hXs : M.IsSkewFamily Xs) (h : ∀ (i : η), Xs i ⊆ R) : (M.restrict R).IsSkewFamily Xs

theorem Matroid.isSkewFamily_restrict_iff' {α : Type u_1} {η : Type u_2} {M : Matroid α} {Xs : η → Set α} {R : Set α} : (M.restrict R).IsSkewFamily Xs ↔ (M.IsSkewFamily fun (i : η) => Xs i ∩ M.E) ∧ ∀ (i : η), Xs i ⊆ R

theorem Matroid.isSkewFamily_restrict_iff {α : Type u_1} {η : Type u_2} {M : Matroid α} {Xs : η → Set α} {R : Set α} (hXs : ∀ (i : η), Xs i ⊆ M.E) : (M.restrict R).IsSkewFamily Xs ↔ M.IsSkewFamily Xs ∧ ∀ (i : η), Xs i ⊆ R

theorem Matroid.isSkewFamily_dual_iff_isModularFamily_compl {α : Type u_1} {η : Type u_2} {M : Matroid α} {X : η → Set α} (hX : ∀ (i : η), X i ⊆ M.E) (hdj : Pairwise (Function.onFun Disjoint X)) : M✶.IsSkewFamily X ↔ M.IsModularFamily fun (i : η) => M.E \ X i

theorem Matroid.Indep.isSkewFamily_iff_pairwise_disjoint {α : Type u_1} {η : Type u_2} {M : Matroid α} {Is : η → Set α} (hI : M.Indep (⋃ (i : η), Is i)) : M.IsSkewFamily Is ↔ Pairwise (Function.onFun Disjoint Is)

theorem Matroid.Indep.isSkewFamily_iff_pairwise_disjoint_union_indep {α : Type u_1} {η : Type u_2} {M : Matroid α} {Is : η → Set α} (hI : ∀ (i : η), M.Indep (Is i)) : M.IsSkewFamily Is ↔ Pairwise (Function.onFun Disjoint Is) ∧ M.Indep (⋃ (i : η), Is i)

theorem Matroid.IsSkewFamily.iUnion_indep_subset_indep {α : Type u_1} {M : Matroid α} {ι : Type u} {Is Xs : ι → Set α} (h : M.IsSkewFamily Xs) (hIX : ∀ (i : ι), Is i ⊆ Xs i) (hIs : ∀ (i : ι), M.Indep (Is i)) : M.Indep (⋃ (i : ι), Is i)

For a skew family Xs, the union of some independent subsets of the Xs is independent. Quite a nasty proof. Probably the right proof involves relating modularity to the lattice of Flats.

theorem Matroid.IsSkewFamily.mono {α : Type u_1} {M : Matroid α} {ι : Type u} {Xs Ys : ι → Set α} (h : M.IsSkewFamily Xs) (hYX : ∀ (i : ι), Ys i ⊆ Xs i) : M.IsSkewFamily Ys

theorem Matroid.isSkewFamily_delete_iff {α : Type u_1} {η : Type u_2} {M : Matroid α} {Xs : η → Set α} {D : Set α} : (M.delete D).IsSkewFamily Xs ↔ (M.IsSkewFamily fun (i : η) => Xs i \ D) ∧ ∀ (i : η), Disjoint (Xs i) D

theorem Matroid.isSkewFamily_delete_iff_of_disjoint {α : Type u_1} {η : Type u_2} {M : Matroid α} {Xs : η → Set α} {D : Set α} (hdj : ∀ (i : η), Disjoint (Xs i) D) : (M.delete D).IsSkewFamily Xs ↔ M.IsSkewFamily Xs

theorem Matroid.isSkewFamily_iff_cls_isSkewFamily {α : Type u_1} {ι : Type u_3} {M : Matroid α} {Xs : ι → Set α} (hX : ∀ (i : ι), Xs i ⊆ M.E) : M.IsSkewFamily Xs ↔ M.IsSkewFamily fun (i : ι) => M.closure (Xs i)

theorem Matroid.isSkewFamily_iff_diff_loops_isSkewFamily {α : Type u_1} {ι : Type u_3} {M : Matroid α} {Xs : ι → Set α} : M.IsSkewFamily Xs ↔ M.IsSkewFamily fun (i : ι) => Xs i \ M.loops

theorem Matroid.IsSkewFamily.iUnion_isBasis_iUnion {α : Type u_1} {ι : Type u_3} {M : Matroid α} {Xs Is : ι → Set α} (h : M.IsSkewFamily Xs) (hIs : ∀ (i : ι), M.IsBasis (Is i) (Xs i)) : M.IsBasis (⋃ (i : ι), Is i) (⋃ (i : ι), Xs i)

theorem Matroid.IsSkewFamily.isModularFamily_union_of_subset {α : Type u_1} {η : Type u_2} {M : Matroid α} {Xs : η → Set α} {Z : Set α} (hX : M.IsSkewFamily Xs) (hZ : Z ⊆ ⋃ (i : η), Xs i) : M.IsModularFamily fun (i : η) => Xs i ∪ Z

theorem Matroid.IsSkewFamily.sum_eRk_eq_eRk_iUnion {α : Type u_1} {η : Type u_2} {M : Matroid α} [Fintype η] {Xs : η → Set α} (h : M.IsSkewFamily Xs) : ∑ i : η, M.eRk (Xs i) = M.eRk (⋃ (i : η), Xs i)

theorem Matroid.IsSkewFamily.sum_eRk_eq_eRk_biUnion {α : Type u_1} {M : Matroid α} {ι : Type u_4} {X : ι → Set α} (s : Finset ι) (h : M.IsSkewFamily fun (i : ι) => X i) : ∑ i ∈ s, M.eRk (X i) = M.eRk (⋃ i ∈ s, X i)

theorem Matroid.IsRkFinite.isSkewFamily_iff_sum_eRk_eq_eRk_iUnion {α : Type u_1} {η : Type u_2} {M : Matroid α} [Fintype η] {Xs : η → Set α} (hXs : ∀ (i : η), M.IsRkFinite (Xs i)) (hXE : ∀ (i : η), Xs i ⊆ M.E) : M.IsSkewFamily Xs ↔ ∑ i : η, M.eRk (Xs i) = M.eRk (⋃ (i : η), Xs i)

theorem Matroid.isSkewFamily_iff_sum_eRk_eq_eRk_iUnion {α : Type u_1} {η : Type u_2} {M : Matroid α} [Fintype η] [M.RankFinite] {Xs : η → Set α} (hXs : ∀ (i : η), Xs i ⊆ M.E) : M.IsSkewFamily Xs ↔ ∑ i : η, M.rk (Xs i) = M.rk (⋃ (i : η), Xs i)

theorem Matroid.isSkewFamily_of_nearly_all_loops {α : Type u_1} {η : Type u_2} {M : Matroid α} {i₀ : η} {Xs : η → Set α} (hi₀ : Xs i₀ ⊆ M.E) (hX : ∀ (i : η), i ≠ i₀ → Xs i ⊆ M.loops) : M.IsSkewFamily Xs

If a family of sets contains at most one set without loops, then the family is skew.

@[simp]

theorem Matroid.isSkewFamily_loopyOn_iff {α : Type u_1} {η : Type u_2} {E : Set α} {Xs : η → Set α} : (loopyOn E).IsSkewFamily Xs ↔ ∀ (i : η), Xs i ⊆ E

theorem Matroid.isSkewFamily_iff_forall_isCircuit {α : Type u_1} {η : Type u_2} {M : Matroid α} {Xs : η → Set α} (hXs : ∀ (i : η), Xs i ⊆ M.E) (hdj : Pairwise (Function.onFun Disjoint Xs)) : M.IsSkewFamily Xs ↔ ∀ (C : Set α), M.IsCircuit C → C ⊆ ⋃ (i : η), Xs i → ∃ (i : η), C ⊆ Xs i

theorem Matroid.IsSkewFamily.exists_subset_of_isCircuit {α : Type u_1} {η : Type u_2} {M : Matroid α} {Xs : η → Set α} (h : M.IsSkewFamily Xs) {C : Set α} (hC : M.IsCircuit C) (hCss : C ⊆ ⋃ (i : η), Xs i) : ∃ (i : η), C ⊆ Xs i

theorem Matroid.IsSkewFamily.subset_of_isCircuit_of_mem {α : Type u_1} {η : Type u_2} {M : Matroid α} {e : α} {Xs : η → Set α} (h : M.IsSkewFamily Xs) {C : Set α} {i : η} (hC : M.IsCircuit C) (hCss : C ⊆ ⋃ (i : η), Xs i) (he : e ∈ C) (hei : e ∈ Xs i) : C ⊆ Xs i

theorem Matroid.isSkewFamily_iff_restrict_iUnion_eq_disjointSigma {α : Type u_1} {M : Matroid α} {ι : Type u_4} {Xs : ι → Set α} (hdj : Pairwise (Function.onFun Disjoint Xs)) (hss : ∀ (i : ι), Xs i ⊆ M.E) : M.IsSkewFamily Xs ↔ M.restrict (⋃ (i : ι), Xs i) = Matroid.disjointSigma (fun (i : ι) => M.restrict (Xs i)) ⋯

theorem Matroid.IsSkewFamily.restrict_iUnion_eq_disjointSigma {α : Type u_1} {M : Matroid α} {ι : Type u_4} {Xs : ι → Set α} (h : M.IsSkewFamily Xs) (hdj : Pairwise (Function.onFun Disjoint Xs)) : M.restrict (⋃ (i : ι), Xs i) = Matroid.disjointSigma (fun (i : ι) => M.restrict (Xs i)) ⋯

theorem Matroid.contract_isSkewFamily_iff_project_isSkewFamily {α : Type u_1} {η : Type u_2} {M : Matroid α} {C : Set α} {Xs : η → Set α} (hXC : ∀ (i : η), Disjoint (Xs i) C) : (M.contract C).IsSkewFamily Xs ↔ (M.project C).IsSkewFamily Xs

theorem Matroid.project_isSkewFamily_iff {α : Type u_1} {ι : Type u_3} {M : Matroid α} {C : Set α} {Xs : ι → Set α} (hC : C ⊆ M.E := by aesop_mat) : (M.project C).IsSkewFamily Xs ↔ (M.IsModularFamily fun (i : ι) => Xs i ∪ C) ∧ ∀ ⦃i j : ι⦄, i ≠ j → Xs i ∩ Xs j ⊆ M.closure C

theorem Matroid.contract_isSkewFamily_iff {α : Type u_1} {η : Type u_2} {M : Matroid α} {C : Set α} {Xs : η → Set α} (hXC : ∀ (i : η), Disjoint (Xs i) C) (hC : C ⊆ M.E := by aesop_mat) : (M.contract C).IsSkewFamily Xs ↔ (M.IsModularFamily fun (i : η) => Xs i ∪ C) ∧ ∀ ⦃i j : η⦄, i ≠ j → Xs i ∩ Xs j ⊆ M.closure C

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

Two sets are skew if they have disjoint bases with independent union.

Equations

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

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

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

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

theorem Matroid.skew_iff_isModularPair_inter_subset_loops {α : Type u_1} {M : Matroid α} {X Y : Set α} : M.Skew X Y ↔ M.IsModularPair X Y ∧ X ∩ Y ⊆ M.loops

theorem Matroid.IsModularPair.skew_of_inter_subset_loops {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsModularPair X Y) (hss : X ∩ Y ⊆ M.loops) : M.Skew X Y

theorem Matroid.IsModularPair.skew_of_disjoint {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.IsModularPair X Y) (hdj : Disjoint X Y) : M.Skew X Y

theorem Matroid.Skew.inter_subset_loops {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.Skew X Y) : X ∩ Y ⊆ M.loops

theorem Matroid.Skew.disjoint {α : Type u_1} {M : Matroid α} {X Y : Set α} [M.Loopless] (h : M.Skew X Y) : Disjoint X Y

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

theorem Matroid.skew_comm {α : Type u_1} {M : Matroid α} {X Y : Set α} : M.Skew X Y ↔ M.Skew Y X

theorem Matroid.isSkewFamily_bool_iff {α : Type u_1} {M : Matroid α} (i : Bool) {X : Bool → Set α} : M.IsSkewFamily X ↔ M.Skew (X i) (X !i)

theorem Matroid.IsSkewFamily.skew_of_ne {α : Type u_1} {ι : Type u_3} {M : Matroid α} {Xs : ι → Set α} {i j : ι} (h : M.IsSkewFamily Xs) (hij : i ≠ j) : M.Skew (Xs i) (Xs j)

theorem Matroid.Skew.disjoint_of_indep_subset_left {α : Type u_1} {M : Matroid α} {I X Y : Set α} (h : M.Skew X Y) (hI : M.Indep I) (hIX : I ⊆ X) : Disjoint I Y

theorem Matroid.Skew.disjoint_of_indep_subset_right {α : Type u_1} {M : Matroid α} {J X Y : Set α} (h : M.Skew X Y) (hJ : M.Indep J) (hJY : J ⊆ Y) : Disjoint X J

theorem Matroid.Skew.disjoint_of_isBasis_of_subset {α : Type u_1} {M : Matroid α} {I J X Y : Set α} (h : M.Skew X Y) (hI : M.IsBasis I X) (hJ : J ⊆ Y) : Disjoint I J

theorem Matroid.Skew.disjoint_of_indep_left {α : Type u_1} {M : Matroid α} {I X : Set α} (h : M.Skew I X) (hI : M.Indep I) : Disjoint I X

theorem Matroid.Skew.disjoint_of_indep_right {α : Type u_1} {M : Matroid α} {I X : Set α} (h : M.Skew X I) (hI : M.Indep I) : Disjoint X I

theorem Matroid.Skew.diff_loops_disjoint_left {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.Skew X Y) : Disjoint (X \ M.loops) Y

theorem Matroid.Skew.diff_loops_disjoint_right {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.Skew X Y) : Disjoint X (Y \ M.loops)

theorem Matroid.Skew.diff_loops_disjoint {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.Skew X Y) : Disjoint (X \ M.loops) (Y \ M.loops)

theorem Matroid.Skew.mono {α : Type u_1} {M : Matroid α} {X X' Y Y' : Set α} (h : M.Skew X Y) (hX : X' ⊆ X) (hY : Y' ⊆ Y) : M.Skew X' Y'

theorem Matroid.Skew.mono_left {α : Type u_1} {M : Matroid α} {X X' Y : Set α} (h : M.Skew X Y) (hX : X' ⊆ X) : M.Skew X' Y

theorem Matroid.Skew.mono_right {α : Type u_1} {M : Matroid α} {X Y Y' : Set α} (h : M.Skew X Y) (hY : Y' ⊆ Y) : M.Skew X Y'

theorem Matroid.skew_anti_left {α : Type u_1} {M : Matroid α} {Y : Set α} : Antitone fun (X : Set α) => M.Skew X Y

theorem Matroid.skew_anti_right {α : Type u_1} {M : Matroid α} {X : Set α} : Antitone fun (Y : Set α) => M.Skew X Y

theorem Matroid.skew_iff_exist_isBases {α : Type u_1} {M : Matroid α} {X Y : Set α} : M.Skew X Y ↔ ∃ (I : Set α) (J : Set α), Disjoint I J ∧ M.IsBasis (I ∪ J) (X ∪ Y) ∧ M.IsBasis I X ∧ M.IsBasis J Y

theorem Matroid.Skew.eRelRk_eq_right {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.Skew X Y) : M.eRelRk X (X ∪ Y) = M.eRk Y

theorem Matroid.Skew.eRelRk_eq_left {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.Skew X Y) : M.eRelRk Y (X ∪ Y) = M.eRk X

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

theorem Matroid.skew_iff_closure_skew {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : X ⊆ M.E := by aesop_mat) (hY : Y ⊆ M.E := by aesop_mat) : M.Skew X Y ↔ M.Skew (M.closure X) (M.closure Y)

theorem Matroid.skew_iff_closure_skew_left {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : X ⊆ M.E := by aesop_mat) : M.Skew X Y ↔ M.Skew (M.closure X) Y

theorem Matroid.skew_iff_closure_skew_right {α : Type u_1} {M : Matroid α} {X Y : Set α} (hY : Y ⊆ M.E := by aesop_mat) : M.Skew X Y ↔ M.Skew X (M.closure Y)

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

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

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

theorem Matroid.skew_iff_of_isLoopEquiv {α : Type u_1} {M : Matroid α} {X X' Y Y' : Set α} (hX : M.IsLoopEquiv X X') (hY : M.IsLoopEquiv Y Y') : M.Skew X Y ↔ M.Skew X' Y'

theorem Matroid.skew_iff_diff_loops_skew {α : Type u_1} {M : Matroid α} {X Y : Set α} : M.Skew X Y ↔ M.Skew (X \ M.loops) (Y \ M.loops)

theorem Matroid.skew_iff_diff_loops_skew_left {α : Type u_1} {M : Matroid α} {X Y : Set α} : M.Skew X Y ↔ M.Skew (X \ M.loops) Y

theorem Matroid.skew_iff_skew_diff_left {α : Type u_1} {M : Matroid α} {X Y : Set α} : M.Skew X Y ↔ M.Skew (X \ Y) Y ∧ X ∩ Y ⊆ M.loops

theorem Matroid.skew_iff_skew_diff_diff {α : Type u_1} {M : Matroid α} {X Y : Set α} : M.Skew X Y ↔ M.Skew (X \ Y) (Y \ X) ∧ X ∩ Y ⊆ M.loops

theorem Matroid.skew_iff_isBases_skew {α : Type u_1} {M : Matroid α} {I J X Y : Set α} (hI : M.IsBasis I X) (hJ : M.IsBasis J Y) : M.Skew I J ↔ M.Skew X Y

theorem Matroid.skew_dual_iff {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXY : Disjoint X Y) (hX : X ⊆ M.E := by aesop_mat) (hY : Y ⊆ M.E := by aesop_mat) : M✶.Skew X Y ↔ M.IsModularPair (M.E \ X) (M.E \ Y)

theorem Matroid.isModularPair_dual_iff {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXY : X ∪ Y = M.E) : M✶.IsModularPair X Y ↔ M.Skew (M.E \ X) (M.E \ Y)

theorem Matroid.Coindep.skew_dual_iff {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : M.Coindep X) (hXY : Disjoint X Y) (hYE : Y ⊆ M.E := by aesop_mat) : M✶.Skew X Y ↔ X ⊆ M.closure (M.E \ (X ∪ Y))

theorem Matroid.Skew.union_indep_of_indep_subsets {α : Type u_1} {M : Matroid α} {I J X Y : Set α} (h : M.Skew X Y) (hI : M.Indep I) (hIX : I ⊆ X) (hJ : M.Indep J) (hJY : J ⊆ Y) : M.Indep (I ∪ J)

Can we just lose this one by the below?

theorem Matroid.Skew.union_indep {α : Type u_1} {M : Matroid α} {I J : Set α} (h : M.Skew I J) (hI : M.Indep I) (hJ : M.Indep J) : M.Indep (I ∪ J)

theorem Matroid.Skew.union_isBasis_union {α : Type u_1} {M : Matroid α} {I J X Y : Set α} (h : M.Skew X Y) (hI : M.IsBasis I X) (hJ : M.IsBasis J Y) : M.IsBasis (I ∪ J) (X ∪ Y)

theorem Matroid.Indep.skew_iff_disjoint {α : Type u_1} {M : Matroid α} {I J : Set α} (h : M.Indep (I ∪ J)) : M.Skew I J ↔ Disjoint I J

theorem Matroid.Indep.skew_iff_disjoint_union_indep {α : Type u_1} {M : Matroid α} {I J : Set α} (hI : M.Indep I) (hJ : M.Indep J) : M.Skew I J ↔ Disjoint I J ∧ M.Indep (I ∪ J)

theorem Matroid.Indep.subset_skew_diff {α : Type u_1} {M : Matroid α} {I J : Set α} (h : M.Indep I) (hJI : J ⊆ I) : M.Skew J (I \ J)

theorem Matroid.skew_iff_contract_restrict_eq_restrict {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : X ⊆ M.E := by aesop_mat) (hY : Y ⊆ M.E := by aesop_mat) : M.Skew X Y ↔ (M.contract X).restrict Y = M.restrict Y

theorem Matroid.Indep.skew_iff_contract_indep {α : Type u_1} {M : Matroid α} {I X : Set α} (hI : M.Indep I) (hX : X ⊆ M.E) : M.Skew I X ↔ (M.contract X).Indep I

theorem Matroid.skew_insert_iff {α : Type u_1} {M : Matroid α} {e : α} {X Y : Set α} (he : e ∈ M.E) : M.Skew (insert e X) Y ↔ M.Skew X Y ∧ (e ∈ M.closure (X ∪ Y) → e ∈ M.closure X)

theorem Matroid.Skew.contract_restrict_eq {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXY : M.Skew X Y) : (M.contract X).restrict Y = M.restrict Y

theorem Matroid.empty_skew {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E) : M.Skew ∅ X

theorem Matroid.skew_empty {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E) : M.Skew X ∅

theorem Matroid.Skew.closure_union_right_inter_left {α : Type u_1} {M : Matroid α} {X Y S : Set α} (h : M.Skew X Y) (hS : S ⊆ X) : M.closure (S ∪ Y) ∩ X = M.closure S ∩ X

theorem Matroid.Skew.closure_union_left_inter_right {α : Type u_1} {M : Matroid α} {X Y S : Set α} (h : M.Skew X Y) (hS : S ⊆ Y) : M.closure (S ∪ X) ∩ Y = M.closure S ∩ Y

theorem Matroid.exists_contract_indep_to_spanning {α : Type u_1} (M : Matroid α) (X : Set α) (hX : X ⊆ M.E) : ∃ (I : Set α), M.Indep I ∧ Disjoint I X ∧ (M.contract I).restrict X = M.restrict X ∧ (M.contract I).Spanning X

theorem Matroid.exists_isMinor_restrict_corestrict_eq_spanning_cospanning {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E) : ∃ (N : Matroid α), N ≤m M ∧ N.restrict X = M.restrict X ∧ N✶.restrict X = M✶.restrict X ∧ N.Spanning X ∧ N✶.Spanning X

For any set X, we can find a minor in which X is spanning and cospanning, such that both the restrict and corestriction to X are unchanged.

theorem Matroid.IsSkewFamily.skew_compl {α : Type u_1} {η : Type u_2} {M : Matroid α} {Xs : η → Set α} (h : M.IsSkewFamily Xs) (A : Set η) : M.Skew (⋃ i ∈ A, Xs i) (⋃ i ∈ Aᶜ, Xs i)

theorem Matroid.IsSkewFamily.skew_compl_singleton {α : Type u_1} {η : Type u_2} {M : Matroid α} {Xs : η → Set α} (h : M.IsSkewFamily Xs) (i : η) : M.Skew (Xs i) (⋃ j ∈ {i}ᶜ, Xs j)

theorem Matroid.IsSkewFamily.isMutualBasis_of_indep {α : Type u_1} {η : Type u_2} {M : Matroid α} {B : Set α} {Xs : η → Set α} (h : M.IsSkewFamily Xs) (hB : M.Indep B) (hBX : B ⊆ ⋃ (i : η), Xs i) (hX : ∀ (i : η), Xs i ⊆ M.closure B) : M.IsMutualBasis B Xs

Can this be moved up?

theorem Matroid.IsSkewFamily.project {α : Type u_1} {η : Type u_2} {M : Matroid α} {Xs : η → Set α} {C : Set α} (h : M.IsSkewFamily Xs) (hC : C ⊆ ⋃ (i : η), Xs i) : (M.project C).IsSkewFamily Xs

theorem Matroid.dual_isSkewFamily_iff {α : Type u_1} {η : Type u_2} {M : Matroid α} {X : η → Set α} (hdj : Pairwise (Function.onFun Disjoint X)) (hu : ⋃ (i : η), X i = M.E) : M✶.IsSkewFamily X ↔ M.IsSkewFamily X

theorem Matroid.skew_iff_forall_isCircuit {α : Type u_1} {M : Matroid α} {X Y : Set α} (hdj : Disjoint X Y) (hX : X ⊆ M.E := by aesop_mat) (hY : Y ⊆ M.E := by aesop_mat) : M.Skew X Y ↔ ∀ (C : Set α), M.IsCircuit C → C ⊆ X ∪ Y → C ⊆ X ∨ C ⊆ Y

theorem Matroid.Skew.subset_or_subset_of_isCircuit {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.Skew X Y) {C : Set α} (hC : M.IsCircuit C) (hCss : C ⊆ X ∪ Y) : C ⊆ X ∨ C ⊆ Y

theorem Matroid.Skew.subset_of_isCircuit_of_mem_left {α : Type u_1} {M : Matroid α} {e : α} {X Y : Set α} (h : M.Skew X Y) {C : Set α} (hC : M.IsCircuit C) (hCXY : C ⊆ X ∪ Y) (he : e ∈ C) (heX : e ∈ X) : C ⊆ X

theorem Matroid.isSkewFamily_iff_forall_skew_compl_singleton {α : Type u_1} {η : Type u_2} {M : Matroid α} {Xs : η → Set α} : M.IsSkewFamily Xs ↔ ∀ (i : η), M.Skew (Xs i) (⋃ j ∈ {i}ᶜ, Xs j)

theorem Matroid.isSkewFamily_set_coe_iff_forall_skew_compl_singleton {α : Type u_1} {η : Type u_2} {M : Matroid α} {I : Set η} (Xs : η → Set α) : (M.IsSkewFamily fun (i : ↑I) => Xs ↑i) ↔ ∀ j ∈ I, M.Skew (Xs j) (⋃ i ∈ I \ {j}, Xs i)

theorem Matroid.isSkewFamily_iff_nearly_forall_skew_compl_singleton {α : Type u_1} {η : Type u_2} {M : Matroid α} {Xs : η → Set α} {i₀ : η} (hi₀ : Xs i₀ ⊆ M.E) : M.IsSkewFamily Xs ↔ ∀ (i : η), i ≠ i₀ → M.Skew (Xs i) (⋃ j ∈ {i}ᶜ, Xs j)

If X i is skew to the union of the other X j for all but one i, then the X i are skew.

theorem Matroid.skew_of_subset_loops {α : Type u_1} {M : Matroid α} {X L : Set α} (hL : L ⊆ M.loops) (hX : X ⊆ M.E) : M.Skew L X

theorem Matroid.skew_project_self {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : X ⊆ M.E := by aesop_mat) (hY : Y ⊆ M.E := by aesop_mat) : (M.project X).Skew X Y

theorem Matroid.IsLoop.skew {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (he : M.IsLoop e) (hX : X ⊆ M.E) : M.Skew {e} X

theorem Matroid.skew_of_subset_coloops {α : Type u_1} {M : Matroid α} {X K : Set α} (hK : K ⊆ M.coloops) (hX : X ⊆ M.E) (hdj : Disjoint K X) : M.Skew K X

theorem Matroid.IsColoop.skew {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (he : M.IsColoop e) (hX : X ⊆ M.E) (heX : e ∉ X) : M.Skew {e} X

theorem Matroid.IsNonloop.skew_right_iff {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (he : M.IsNonloop e) (hX : X ⊆ M.E := by aesop_mat) : M.Skew X {e} ↔ e ∉ M.closure X

theorem Matroid.IsNonloop.skew_left_iff {α : Type u_1} {M : Matroid α} {e : α} {X : Set α} (he : M.IsNonloop e) (hX : X ⊆ M.E := by aesop_mat) : M.Skew {e} X ↔ e ∉ M.closure X

theorem Matroid.Skew.isModularPair_union_right_of_subset_left {α : Type u_1} {M : Matroid α} {X Y Z : Set α} (hXY : M.Skew X Y) (hZX : Z ⊆ X) : M.IsModularPair X (Y ∪ Z)

theorem Matroid.Skew.isModularPair_union_union_of_subset {α : Type u_1} {M : Matroid α} {X Y Z : Set α} (hXY : M.Skew X Y) (hZX : Z ⊆ X ∪ Y) : M.IsModularPair (X ∪ Z) (Y ∪ Z)

theorem Matroid.Skew.restrict {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXY : M.Skew X Y) (R : Set α) : (M.restrict R).Skew (X ∩ R) (Y ∩ R)

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

theorem Matroid.Skew.of_restrict {α : Type u_1} {M : Matroid α} {X Y R : Set α} (h : (M.restrict R).Skew X Y) (hR : R ⊆ M.E := by aesop_mat) : M.Skew X Y

theorem Matroid.skew_restrict_iff {α : Type u_1} {M : Matroid α} {X Y R : Set α} (hRE : R ⊆ M.E := by aesop_mat) : (M.restrict R).Skew X Y ↔ M.Skew X Y ∧ X ⊆ R ∧ Y ⊆ R

theorem Matroid.Skew.delete {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXY : M.Skew X Y) (D : Set α) : (M.delete D).Skew (X \ D) (Y \ D)

theorem Matroid.Skew.delete_of_disjoint {α : Type u_1} {M : Matroid α} {X Y D : Set α} (hXY : M.Skew X Y) (hXD : Disjoint X D) (hYD : Disjoint Y D) : (M.delete D).Skew X Y

theorem Matroid.Skew.of_delete {α : Type u_1} {M : Matroid α} {X Y D : Set α} (h : (M.delete D).Skew X Y) : M.Skew X Y

theorem Matroid.skew_delete_iff {α : Type u_1} {M : Matroid α} {X Y D : Set α} : (M.delete D).Skew X Y ↔ M.Skew X Y ∧ Disjoint X D ∧ Disjoint Y D

theorem Matroid.isModularPair_iff_skew_contract_inter {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXY : X ∩ Y ⊆ M.E) : M.IsModularPair X Y ↔ (M.contract (X ∩ Y)).Skew (X \ Y) (Y \ X)

theorem Matroid.contract_skew_iff_project_skew {α : Type u_1} {M : Matroid α} {X Y C : Set α} (hXC : Disjoint X C) (hYC : Disjoint Y C) : (M.contract C).Skew X Y ↔ (M.project C).Skew X Y

theorem Matroid.contract_skew_iff {α : Type u_1} {M : Matroid α} {X Y C : Set α} (hXC : Disjoint X C) (hYC : Disjoint Y C) (hC : C ⊆ M.E := by aesop_mat) : (M.contract C).Skew X Y ↔ M.IsModularPair (X ∪ C) (Y ∪ C) ∧ X ∩ Y ⊆ M.closure C

theorem Matroid.Skew.contract_subset_left {α : Type u_1} {M : Matroid α} {X Y C : Set α} (hXY : M.Skew X Y) (hCX : C ⊆ X) : (M.contract C).Skew (X \ C) (Y \ C)

theorem Matroid.Skew.contract_subset_left_of_disjoint_loops {α : Type u_1} {M : Matroid α} {X Y C : Set α} (hXY : M.Skew X Y) (hCX : C ⊆ X) (hY : Disjoint Y M.loops) : (M.contract C).Skew (X \ C) Y

theorem Matroid.Skew.contract_subset_right_of_disjoint_loops {α : Type u_1} {M : Matroid α} {X Y C : Set α} (hXY : M.Skew X Y) (hCY : C ⊆ Y) (hX : Disjoint X M.loops) : (M.contract C).Skew X (Y \ C)

theorem Matroid.Skew.contract_subset_right {α : Type u_1} {M : Matroid α} {X Y C : Set α} (hXY : M.Skew X Y) (hCX : C ⊆ Y) : (M.contract C).Skew (X \ C) (Y \ C)

theorem Matroid.Skew.contract_subset_union {α : Type u_1} {M : Matroid α} {X Y C : Set α} (hXY : M.Skew X Y) (hC : C ⊆ X ∪ Y) : (M.contract C).Skew (X \ C) (Y \ C)

theorem Matroid.IsModularPair.contract_subset_union {α : Type u_1} {M : Matroid α} {X Y C : Set α} (hXY : M.IsModularPair X Y) (hC : C ⊆ X ∪ Y) : (M.contract C).IsModularPair (X \ C) (Y \ C)

theorem Matroid.IsModularPair.skew_contract_inter {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXY : M.IsModularPair X Y) : (M.contract (X ∩ Y)).Skew (X \ Y) (Y \ X)

theorem Matroid.skew_iff_restrict_union_eq {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXE : X ⊆ M.E) (hYE : Y ⊆ M.E) (hdj : Disjoint X Y) : M.Skew X Y ↔ M.restrict (X ∪ Y) = (M.restrict X).disjointSum (M.restrict Y) hdj

theorem Matroid.skew_disjointSum {α : Type u_1} {M₁ M₂ : Matroid α} (hdj : Disjoint M₁.E M₂.E) : (M₁.disjointSum M₂ hdj).Skew M₁.E M₂.E

theorem Matroid.contract_eq_delete_iff_skew_compl {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E := by aesop_mat) : M.contract X = M.delete X ↔ M.Skew X (M.E \ X)

theorem Matroid.skew_iff_of_subset_left {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXY : X ⊆ Y) (hY : Y ⊆ M.E := by aesop_mat) : M.Skew X Y ↔ X ⊆ M.loops

theorem Matroid.skew_iff_of_subset_right {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXY : X ⊆ Y) (hY : Y ⊆ M.E := by aesop_mat) : M.Skew Y X ↔ X ⊆ M.loops

theorem Matroid.Coindep.skew_compl_iff_subset_loops {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Coindep X) : M.Skew X (M.E \ X) ↔ X ⊆ M.loops

theorem Matroid.Indep.skew_compl_iff_subset_coloops {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) : M.Skew I (M.E \ I) ↔ I ⊆ M.coloops

theorem Matroid.Spanning.skew_iff_left {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : M.Spanning X) (hY : Y ⊆ M.E := by aesop_mat) : M.Skew X Y ↔ Y ⊆ M.loops

theorem Matroid.Spanning.skew_iff_right {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : M.Spanning X) (hY : Y ⊆ M.E := by aesop_mat) : M.Skew Y X ↔ Y ⊆ M.loops

theorem Matroid.skew_iff_forall_isCircuit_of_inter_subset_loops {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : X ⊆ M.E := by aesop_mat) (hY : Y ⊆ M.E := by aesop_mat) : M.Skew X Y ↔ X ∩ Y ⊆ M.loops ∧ ∀ (C : Set α), M.IsCircuit C → C ⊆ X ∪ Y → C ⊆ X ∨ C ⊆ Y

theorem Matroid.Skew.isCircuit_contract {α : Type u_1} {M : Matroid α} {X C : Set α} (hXC : M.Skew X C) (hC : M.IsCircuit C) (hdj : Disjoint X C) : (M.contract X).IsCircuit C

theorem Matroid.Skew.isCircuit_contract_of_nontrivial {α : Type u_1} {M : Matroid α} {X C : Set α} (hXC : M.Skew X C) (hC : M.IsCircuit C) (hCnt : C.Nontrivial) : (M.contract X).IsCircuit C

theorem Matroid.IsCircuit.isCircuit_contract_iff_skew {α : Type u_1} {M : Matroid α} {X C : Set α} (hC : M.IsCircuit C) (hXC : Disjoint X C) (hX : X ⊆ M.E := by aesop_mat) : (M.contract X).IsCircuit C ↔ M.Skew X C

theorem Matroid.IsCircuit.isCircuit_contract_iff_skew_of_nontrivial {α : Type u_1} {M : Matroid α} {X C : Set α} (hC : M.IsCircuit C) (hnt : C.Nontrivial) (hX : X ⊆ M.E := by aesop_mat) : (M.contract X).IsCircuit C ↔ M.Skew X C

theorem Matroid.IsTriangle.isTriangle_contract_iff_skew {α : Type u_1} {M : Matroid α} {X T : Set α} (hT : M.IsTriangle T) (hX : X ⊆ M.E := by aesop_mat) : (M.contract X).IsTriangle T ↔ M.Skew X T

theorem Matroid.IsTriangle.contract_isTriangle {α : Type u_1} {M : Matroid α} {X T : Set α} (hT : M.IsTriangle T) (hX : M.Skew X T) : (M.contract X).IsTriangle T

theorem Matroid.IsCircuit.contractElem_isCircuit_of_notMem_closure {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} (hC : M.IsCircuit C) (heC : e ∉ M.closure C) : (M.contract {e}).IsCircuit C

theorem Matroid.IsTriangle.contractElem_isTriangle_of_notMem_closure {α : Type u_1} {M : Matroid α} {e : α} {T : Set α} (hT : M.IsTriangle T) (he : e ∉ M.closure T) : (M.contract {e}).IsTriangle T

theorem Matroid.isCircuit_contractElem_iff_of_notMem {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} (heC : e ∉ C) (he : M.IsNonloop e) : (M.contract {e}).IsCircuit C ↔ M.IsCircuit C ∧ e ∉ M.closure C ∨ M.IsCircuit (insert e C)

theorem Matroid.Indep.contract_indep_iff_skew {α : Type u_1} {M : Matroid α} {I C : Set α} (hI : M.Indep I) (hCE : C ⊆ M.E := by aesop_mat) : (M.contract C).Indep I ↔ M.Skew I C

theorem Matroid.contract_indep_iff_indep_skew {α : Type u_1} {M : Matroid α} {I X : Set α} (hXE : X ⊆ M.E := by aesop_mat) : (M.contract X).Indep I ↔ M.Indep I ∧ M.Skew I X

theorem Matroid.project_indep_iff_indep_skew {α : Type u_1} {M : Matroid α} {I X : Set α} (hXE : X ⊆ M.E := by aesop_mat) : (M.project X).Indep I ↔ M.Indep I ∧ M.Skew I X

theorem Matroid.Indep.skew_of_contract {α : Type u_1} {M : Matroid α} {I C : Set α} (hI : (M.contract C).Indep I) (hC : C ⊆ M.E := by aesop_mat) : M.Skew I C

theorem Matroid.Indep.skew_of_project {α : Type u_1} {M : Matroid α} {I C : Set α} (hI : (M.project C).Indep I) (hC : C ⊆ M.E := by aesop_mat) : M.Skew I C

theorem Matroid.IsCircuit.exists_isCircuit_mem_subset_union_of_not_skew {α : Type u_1} {M : Matroid α} {e : α} {X C : Set α} (hC : M.IsCircuit C) (hdj : Disjoint C X) (hXC : ¬M.Skew C X) (he : e ∈ C) (hX : X ⊆ M.E := by aesop_mat) : ∃ (C' : Set α), M.IsCircuit C' ∧ C' ⊆ C ∪ X ∧ e ∈ C' ∧ (C' ∩ X).Nonempty

If a circuit C is not skew to a set X, then we can find a circuit contained in C ∪ X that intersects X, and also contains an arbitrary element of C.

structure Matroid.ModularCompl {α : Type u_1} (M : Matroid α) (F₀ F₁ F F' : Set α) : Prop

M.ModularCompl F₀ F₁ F F' means that F,F' are a modular pair of flats with intersection F₀ and whose union has closure F₁. Every F with F₀ ⊆ F ⊆ F₁ has a ModularCompl.

• isFlat_left : M.IsFlat F
• isFlat_right : M.IsFlat F'
• inter_eq : F ∩ F' = F₀
• closure_union_eq : M.closure (F ∪ F') = F₁
• isModularPair : M.IsModularPair F F'

theorem Matroid.modularCompl_iff {α : Type u_1} (M : Matroid α) (F₀ F₁ F F' : Set α) : M.ModularCompl F₀ F₁ F F' ↔ M.IsFlat F ∧ M.IsFlat F' ∧ F ∩ F' = F₀ ∧ M.closure (F ∪ F') = F₁ ∧ M.IsModularPair F F'

theorem Matroid.ModularCompl.symm {α : Type u_1} {M : Matroid α} {F₀ F₁ F F' : Set α} (h : M.ModularCompl F₀ F₁ F F') : M.ModularCompl F₀ F₁ F' F

theorem Matroid.modularCompl_comm {α : Type u_1} {M : Matroid α} {F₀ F₁ F F' : Set α} : M.ModularCompl F₀ F₁ F F' ↔ M.ModularCompl F₀ F₁ F' F

theorem Matroid.ModularCompl.left_subset_ground {α : Type u_1} {M : Matroid α} {F₀ F₁ F F' : Set α} (h : M.ModularCompl F₀ F₁ F F') : F ⊆ M.E

theorem Matroid.ModularCompl.right_subset_ground {α : Type u_1} {M : Matroid α} {F₀ F₁ F F' : Set α} (h : M.ModularCompl F₀ F₁ F F') : F' ⊆ M.E

theorem Matroid.ModularCompl.isFlat_top {α : Type u_1} {M : Matroid α} {F₀ F₁ F F' : Set α} (h : M.ModularCompl F₀ F₁ F F') : M.IsFlat F₁

theorem Matroid.ModularCompl.top_subset_ground {α : Type u_1} {M : Matroid α} {F₀ F₁ F F' : Set α} (h : M.ModularCompl F₀ F₁ F F') : F₁ ⊆ M.E

theorem Matroid.ModularCompl.isFlat_bot {α : Type u_1} {M : Matroid α} {F₀ F₁ F F' : Set α} (h : M.ModularCompl F₀ F₁ F F') : M.IsFlat F₀

theorem Matroid.ModularCompl.bot_subset_ground {α : Type u_1} {M : Matroid α} {F₀ F₁ F F' : Set α} (h : M.ModularCompl F₀ F₁ F F') : F₀ ⊆ M.E

theorem Matroid.ModularCompl.subset_left {α : Type u_1} {M : Matroid α} {F₀ F₁ F F' : Set α} (h : M.ModularCompl F₀ F₁ F F') : F₀ ⊆ F

theorem Matroid.ModularCompl.subset_right {α : Type u_1} {M : Matroid α} {F₀ F₁ F F' : Set α} (h : M.ModularCompl F₀ F₁ F F') : F₀ ⊆ F'

theorem Matroid.ModularCompl.left_subset {α : Type u_1} {M : Matroid α} {F₀ F₁ F F' : Set α} (h : M.ModularCompl F₀ F₁ F F') : F ⊆ F₁

theorem Matroid.ModularCompl.right_subset {α : Type u_1} {M : Matroid α} {F₀ F₁ F F' : Set α} (h : M.ModularCompl F₀ F₁ F F') : F' ⊆ F₁

theorem Matroid.ModularCompl.subset {α : Type u_1} {M : Matroid α} {F₀ F₁ F F' : Set α} (h : M.ModularCompl F₀ F₁ F F') : F₀ ⊆ F₁

theorem Matroid.IsFlat.exists_modularCompl {α : Type u_1} {M : Matroid α} {F₀ F₁ F : Set α} (hF₀ : M.IsFlat F₀) (hF₁ : M.IsFlat F₁) (hF : M.IsFlat F) (hF₀F : F₀ ⊆ F) (hFF₁ : F ⊆ F₁) : ∃ (F' : Set α), M.ModularCompl F₀ F₁ F F'

theorem Matroid.modularCompl_loops_ground_iff {α : Type u_1} {M : Matroid α} {F F' : Set α} (hF : M.IsFlat F) (hF' : M.IsFlat F') : M.ModularCompl M.loops M.E F F' ↔ M.Skew F F' ∧ M.Spanning (F ∪ F')

Two flats are ModularCompl in the interval [M.loops, M.E] iff they are skew with spanning union.

theorem Matroid.ModularCompl.isBasis_inter_isBasis_eq {α : Type u_1} {M : Matroid α} {I J F₀ F₁ F F' J' : Set α} (h : M.ModularCompl F₀ F₁ F F') (hI : M.IsBasis I F₀) (hJ : M.IsBasis J F) (hJ' : M.IsBasis J' F') (hIJ : I ⊆ J) (hIJ' : I ⊆ J') : J ∩ J' = I

theorem Matroid.ModularCompl.isBasis_inter_right_eq {α : Type u_1} {M : Matroid α} {I J F₀ F₁ F F' : Set α} (h : M.ModularCompl F₀ F₁ F F') (hI : M.IsBasis I F₀) (hJ : M.IsBasis J F) (hIJ : I ⊆ J) : J ∩ F' = I

theorem Matroid.ModularCompl.union_isBasis_top {α : Type u_1} {M : Matroid α} {I J F₀ F₁ F F' J' : Set α} (h : M.ModularCompl F₀ F₁ F F') (hI : M.IsBasis I F₀) (hJ : M.IsBasis J F) (hJ' : M.IsBasis J' F') (hIJ : I ⊆ J) (hIJ' : I ⊆ J') : M.IsBasis (J ∪ J') F₁