def Matroid.IsHyperplane {α : Type u_1} (M : Matroid α) (H : Set α) : Prop

A hyperplane is a maximal set containing no base

Equations

• M.IsHyperplane H = (H ⋖[M] M.E)

theorem Matroid.IsHyperplane.subset_ground {α : Type u_1} {M : Matroid α} {H : Set α} (hH : M.IsHyperplane H) : H ⊆ M.E

theorem Matroid.isHyperplane_iff_covBy {α : Type u_1} {M : Matroid α} {H : Set α} : M.IsHyperplane H ↔ H ⋖[M] M.E

theorem Matroid.IsHyperplane.covBy {α : Type u_1} {M : Matroid α} {H : Set α} (h : M.IsHyperplane H) : H ⋖[M] M.E

theorem Matroid.IsHyperplane.isFlat {α : Type u_1} {M : Matroid α} {H : Set α} (hH : M.IsHyperplane H) : M.IsFlat H

theorem Matroid.IsHyperplane.ssubset_ground {α : Type u_1} {M : Matroid α} {H : Set α} (hH : M.IsHyperplane H) : H ⊂ M.E

theorem Matroid.IsHyperplane.ssubset_univ {α : Type u_1} {M : Matroid α} {H : Set α} (hH : M.IsHyperplane H) : H ⊂ Set.univ

theorem Matroid.IsFlat.isHyperplane_iff_eRelRk_ground_eq_one {α : Type u_1} {M : Matroid α} {H : Set α} (hH : M.IsFlat H) : M.IsHyperplane H ↔ M.eRelRk H M.E = 1

theorem Matroid.IsHyperplane.closure_insert_eq {α : Type u_1} {M : Matroid α} {H : Set α} {e : α} (hH : M.IsHyperplane H) (heH : e ∉ H) (he : e ∈ M.E := by aesop_mat) : M.closure (insert e H) = M.E

theorem Matroid.IsHyperplane.closure_eq_ground_of_ssuperset {α : Type u_1} {M : Matroid α} {X H : Set α} (hH : M.IsHyperplane H) (hX : H ⊂ X) (hX' : X ⊆ M.E := by aesop_mat) : M.closure X = M.E

theorem Matroid.IsHyperplane.spanning_of_ssuperset {α : Type u_1} {M : Matroid α} {X H : Set α} (hH : M.IsHyperplane H) (hX : H ⊂ X) (hXE : X ⊆ M.E := by aesop_mat) : M.Spanning X

theorem Matroid.IsHyperplane.not_spanning {α : Type u_1} {M : Matroid α} {H : Set α} (hH : M.IsHyperplane H) : ¬M.Spanning H

theorem Matroid.IsHyperplane.nonspanning {α : Type u_1} {M : Matroid α} {H : Set α} (hH : M.IsHyperplane H) : M.Nonspanning H

theorem Matroid.IsHyperplane.isFlat_superset_eq_ground {α : Type u_1} {M : Matroid α} {F H : Set α} (hH : M.IsHyperplane H) (hF : M.IsFlat F) (hHF : H ⊂ F) : F = M.E

theorem Matroid.isHyperplane_iff_maximal_proper_isFlat {α : Type u_1} {M : Matroid α} {H : Set α} : M.IsHyperplane H ↔ Maximal (fun (X : Set α) => M.IsFlat X ∧ X ⊂ M.E) H

theorem Matroid.isHyperplane_iff_maximal_nonspanning {α : Type u_1} {M : Matroid α} {H : Set α} : M.IsHyperplane H ↔ Maximal M.Nonspanning H

instance Matroid.instGroundedPredSetIsHyperplane : GroundedPred fun {α : Type u_2} => IsHyperplane

instance Matroid.instInvariantFunSetPropIsHyperplane : InvariantFun (fun {α : Type u_2} => IsHyperplane) fun {β : Type u_3} => IsHyperplane

theorem Matroid.IsHyperplane.eq_of_subset_nonspanning {α : Type u_1} {M : Matroid α} {X H : Set α} (hH : M.IsHyperplane H) (hX : M.Nonspanning X) (hHX : H ⊆ X) : H = X

@[simp]

theorem Matroid.isCocircuit_compl_iff_isHyperplane {α : Type u_1} {M : Matroid α} {H : Set α} (hH : H ⊆ M.E := by aesop_mat) : M.IsCocircuit (M.E \ H) ↔ M.IsHyperplane H

@[simp]

theorem Matroid.isHyperplane_compl_iff_isCocircuit {α : Type u_1} {M : Matroid α} {K : Set α} (h : K ⊆ M.E := by aesop_mat) : M.IsHyperplane (M.E \ K) ↔ M.IsCocircuit K

theorem Matroid.IsHyperplane.compl_isCocircuit {α : Type u_1} {M : Matroid α} {H : Set α} (hH : M.IsHyperplane H) : M.IsCocircuit (M.E \ H)

theorem Matroid.isHyperplane_dual_iff {α : Type u_1} {M : Matroid α} {H : Set α} (hH : H ⊆ M.E := by aesop_mat) : M✶.IsHyperplane H ↔ M.IsCircuit (M.E \ H)

@[simp]

theorem Matroid.loopyOn_not_isHyperplane {α : Type u_1} (E H : Set α) : ¬(loopyOn E).IsHyperplane H

@[simp]

theorem Matroid.freeOn_isHyperplane_iff {α : Type u_1} (E H : Set α) : (freeOn E).IsHyperplane H ↔ ∃ e ∈ E, H = E \ {e}

theorem Matroid.isHyperplane_compl_dual_iff {α : Type u_1} {M : Matroid α} {H : Set α} (hH : H ⊆ M.E := by aesop_mat) : M✶.IsHyperplane (M.E \ H) ↔ M.IsCircuit H

theorem Matroid.IsCocircuit.compl_isHyperplane {α : Type u_1} {M : Matroid α} {K : Set α} (hK : M.IsCocircuit K) : M.IsHyperplane (M.E \ K)

theorem Matroid.IsCircuit.compl_isHyperplane_dual {α : Type u_1} {M : Matroid α} {C : Set α} (h : M.IsCircuit C) : M✶.IsHyperplane (M.E \ C)

theorem Matroid.Nonspanning.exists_isHyperplane_supset {α : Type u_1} {M : Matroid α} {X : Set α} (h : M.Nonspanning X) : ∃ (H : Set α), X ⊆ H ∧ M.IsHyperplane H

theorem Matroid.nonspanning_iff_exists_isHyperplane_superset {α : Type u_1} {M : Matroid α} {X : Set α} : M.Nonspanning X ↔ ∃ (H : Set α), X ⊆ H ∧ M.IsHyperplane H

theorem Matroid.univ_not_isHyperplane {α : Type u_1} (M : Matroid α) : ¬M.IsHyperplane Set.univ

theorem Matroid.IsHyperplane.eq_of_subset {α : Type u_1} {M : Matroid α} {H₁ H₂ : Set α} (h₁ : M.IsHyperplane H₁) (h₂ : M.IsHyperplane H₂) (h : H₁ ⊆ H₂) : H₁ = H₂

theorem Matroid.IsHyperplane.not_ssubset {α : Type u_1} {M : Matroid α} {H₁ H₂ : Set α} (h₁ : M.IsHyperplane H₁) (h₂ : M.IsHyperplane H₂) : ¬H₁ ⊂ H₂

theorem Matroid.IsHyperplane.inter_ssubset_left_of_ne {α : Type u_1} {M : Matroid α} {H₁ H₂ : Set α} (h₁ : M.IsHyperplane H₁) (h₂ : M.IsHyperplane H₂) (hne : H₁ ≠ H₂) : H₁ ∩ H₂ ⊂ H₁

theorem Matroid.IsHyperplane.inter_ssubset_right_of_ne {α : Type u_1} {M : Matroid α} {H₁ H₂ : Set α} (h₁ : M.IsHyperplane H₁) (h₂ : M.IsHyperplane H₂) (hne : H₁ ≠ H₂) : H₁ ∩ H₂ ⊂ H₂

theorem Matroid.IsBase.isHyperplane_of_closure_diff_singleton {α : Type u_1} {M : Matroid α} {B : Set α} {e : α} (hB : M.IsBase B) (heB : e ∈ B) : M.IsHyperplane (M.closure (B \ {e}))

theorem Matroid.IsHyperplane.ssuperset_eq_univ_of_isFlat {α : Type u_1} {M : Matroid α} {F H : Set α} (hH : M.IsHyperplane H) (hF : M.IsFlat F) (h : H ⊂ F) : F = M.E

theorem Matroid.IsHyperplane.closure_insert_eq_univ {α : Type u_1} {M : Matroid α} {H : Set α} {e : α} (hH : M.IsHyperplane H) (he : e ∈ M.E \ H) : M.closure (insert e H) = M.E

theorem Matroid.exists_isHyperplane_sep_of_notMem_closure {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (h : e ∈ M.E \ M.closure X) (hX : X ⊆ M.E := by aesop_mat) : ∃ (H : Set α), M.IsHyperplane H ∧ X ⊆ H ∧ e ∉ H

theorem Matroid.closure_eq_sInter_isHyperplane {α : Type u_1} (M : Matroid α) (X : Set α) (hX : X ⊆ M.E := by aesop_mat) : M.closure X = ⋂₀ {H : Set α | M.IsHyperplane H ∧ X ⊆ H} ∩ M.E

theorem Matroid.isFlat_iff_eq_sInter_isHyperplanes {α : Type u_1} {M : Matroid α} {F : Set α} : M.IsFlat F ↔ ∃ (Hs : Set (Set α)), (∀ H ∈ Hs, M.IsHyperplane H) ∧ F = ⋂₀ Hs ∩ M.E

theorem Matroid.IsFlat.eq_sInter_isHyperplanes_of_ne_ground {α : Type u_1} {M : Matroid α} {F : Set α} (hF : M.IsFlat F) (hFE : F ≠ M.E) : ∃ (Hs : Set (Set α)), Hs.Nonempty ∧ (∀ H ∈ Hs, M.IsHyperplane H) ∧ F = ⋂₀ Hs

theorem Matroid.mem_closure_iff_forall_isHyperplane {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (hX : X ⊆ M.E := by aesop_mat) (he : e ∈ M.E := by aesop_mat) : e ∈ M.closure X ↔ ∀ (H : Set α), M.IsHyperplane H → X ⊆ H → e ∈ H

theorem Matroid.mem_dual_closure_iff_forall_isCircuit {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (he : e ∈ M.E := by aesop_mat) : e ∈ M✶.closure X ↔ ∀ (C : Set α), M.IsCircuit C → e ∈ C → (X ∩ C).Nonempty

theorem Matroid.mem_dual_closure_iff_notMem_closure_compl {α : Type u_1} {M : Matroid α} {X : Set α} {e : α} (heX : e ∉ X) (heE : e ∈ M.E := by aesop_mat) : e ∈ M✶.closure X ↔ e ∉ M.closure ((M.E \ X) \ {e})

theorem Matroid.IsFlat.subset_isHyperplane_of_ne_ground {α : Type u_1} {M : Matroid α} {F : Set α} (hF : M.IsFlat F) (h : F ≠ M.E) : ∃ (H : Set α), M.IsHyperplane H ∧ F ⊆ H

theorem Matroid.subset_isHyperplane_iff_closure_ne_ground {α : Type u_1} {M : Matroid α} {Y : Set α} (hY : Y ⊆ M.E := by aesop_mat) : M.closure Y ≠ M.E ↔ ∃ (H : Set α), M.IsHyperplane H ∧ Y ⊆ H

theorem Matroid.IsHyperplane.inter_covBy_comm {α : Type u_1} {M : Matroid α} {H₁ H₂ : Set α} (hH₁ : M.IsHyperplane H₁) (hH₂ : M.IsHyperplane H₂) : H₁ ∩ H₂ ⋖[M] H₁ ↔ H₁ ∩ H₂ ⋖[M] H₂

theorem Matroid.IsHyperplane.isBasis_isHyperplane_delete {α : Type u_1} {M : Matroid α} {I H : Set α} (hH : M.IsHyperplane H) (hI : M.IsBasis I H) : (M.delete (H \ I)).IsHyperplane I

theorem Matroid.IsHyperplane.isBasis_isHyperplane_restrict {α : Type u_1} {M : Matroid α} {I H : Set α} (hH : M.IsHyperplane H) (hI : M.IsBasis I H) : (M.restrict (I ∪ M.E \ H)).IsHyperplane I

theorem Matroid.IsHyperplane.eRk_add_one_eq {α : Type u_1} {M : Matroid α} {H : Set α} (hH : M.IsHyperplane H) : M.eRk H + 1 = M.eRank

theorem Matroid.IsHyperplane.insert_isBase_of_isBasis {α : Type u_1} {M : Matroid α} {I H : Set α} {e : α} (hH : M.IsHyperplane H) (hI : M.IsBasis I H) (he : e ∈ M.E \ H) : M.IsBase (insert e I)

theorem Matroid.IsHyperplane.exists_insert_isBase_of_isBasis {α : Type u_1} {M : Matroid α} {I H : Set α} (hH : M.IsHyperplane H) (hI : M.IsBasis I H) : ∃ e ∈ M.E \ H, M.IsBase (insert e I)

theorem Matroid.IsHyperplane.inter_isHyperplane_spanning_restrict {α : Type u_1} {M : Matroid α} {H S : Set α} (hH : M.IsHyperplane H) (hS : M.Spanning S) (hcl : H ⊆ M.closure (H ∩ S)) : (M.restrict S).IsHyperplane (H ∩ S)

theorem Matroid.Spanning.isHyperplane_restrict_iff {α : Type u_1} {M : Matroid α} {H S : Set α} (hS : M.Spanning S) : (M.restrict S).IsHyperplane H ↔ M.IsHyperplane (M.closure H) ∧ H = M.closure H ∩ S

structure Matroid.IsCircuitHyperplane {α : Type u_1} (M : Matroid α) (C : Set α) : Prop

• isCircuit : M.IsCircuit C
• isHyperplane : M.IsHyperplane C

theorem Matroid.isCircuitHyperplane_iff {α : Type u_1} (M : Matroid α) (C : Set α) : M.IsCircuitHyperplane C ↔ M.IsCircuit C ∧ M.IsHyperplane C

instance Matroid.instGroundedPredSetIsCircuitHyperplane : GroundedPred fun {α : Type u_2} => IsCircuitHyperplane

instance Matroid.instInvariantFunSetPropIsCircuitHyperplane : InvariantFun (fun {α : Type u_2} => IsCircuitHyperplane) fun {β : Type u_3} => IsCircuitHyperplane

theorem Matroid.IsCircuitHyperplane.subset_ground {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuitHyperplane C) : C ⊆ M.E

theorem Matroid.IsCircuitHyperplane.compl_dual {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.IsCircuitHyperplane C) : M✶.IsCircuitHyperplane (M.E \ C)

theorem Matroid.isCircuitHyperplane_dual_iff {α : Type u_1} {M : Matroid α} {C : Set α} (hC : C ⊆ M.E := by aesop_mat) : M✶.IsCircuitHyperplane C ↔ M.IsCircuitHyperplane (M.E \ C)

theorem Matroid.isCircuitHyperplane_iff_isCircuit_isCocircuit {α : Type u_1} {M : Matroid α} {C : Set α} : M.IsCircuitHyperplane C ↔ M.IsCircuit C ∧ M.IsCocircuit (M.E \ C)

@[simp]

theorem Matroid.loopyOn_not_isCircuitHyperplane {α : Type u_1} (E C : Set α) : ¬(loopyOn E).IsCircuitHyperplane C

@[simp]

theorem Matroid.freeOn_not_isCircuitHyperplane {α : Type u_1} (E C : Set α) : ¬(freeOn E).IsCircuitHyperplane C

theorem Matroid.IsCircuitHyperplane.contract {α : Type u_1} {M : Matroid α} {X C : Set α} (hX : M.IsCircuitHyperplane X) (hCX : C ⊂ X) : (M.contract C).IsCircuitHyperplane (X \ C)

theorem Matroid.IsCircuitHyperplane.delete {α : Type u_1} {M : Matroid α} {X D : Set α} (hX : M.IsCircuitHyperplane X) (hDX : D ⊂ M.E \ X) : (M.delete D).IsCircuitHyperplane X