def CircPredToIndep {α : Type u_1} (P : Set α → Prop) (E : Set α) (I : Set α) : Prop

Independence predicate derived from circuit predicate P.

Equations

• CircPredToIndep P E I = (I ⊆ E ∧ ∀ (C : Set α), P C → ¬C ⊆ I)

structure ValidXFamily {α : Type u_1} (P : Set α → Prop) (C : Set α) (X : Set α) : Type u_1

Family of circuits satisfying assumptions of circuit condition (C3) from Bruhn et al.

• F : ↑X → Set α
• hPF : ∀ (x : ↑X), P (self.F x)
• hF : ∀ x ∈ X, ∀ (y : ↑X), x ∈ self.F y ↔ x = ↑y

theorem ValidXFamily.hPF {α : Type u_1} {P : Set α → Prop} {C : Set α} {X : Set α} (self : ValidXFamily P C X) (x : ↑X) : P (self.F x)

theorem ValidXFamily.hF {α : Type u_1} {P : Set α → Prop} {C : Set α} {X : Set α} (self : ValidXFamily P C X) (x : α) : x ∈ X → ∀ (y : ↑X), x ∈ self.F y ↔ x = ↑y

theorem ValidXFamily.mem_of_elem {α : Type u_1} {P : Set α → Prop} {C : Set α} {X : Set α} (F : ValidXFamily P C X) (x : ↑X) : ↑x ∈ F.F x

def ValidXFamily.union {α : Type u_1} {P : Set α → Prop} {C : Set α} {X : Set α} (F : ValidXFamily P C X) : Set α

Shorthand for union of sets in ValidXFamily

Equations

• F.union = Set.iUnion F.F

theorem ValidXFamily.outside {α : Type u_1} {P : Set α → Prop} {C : Set α} {X : Set α} {F : ValidXFamily P C X} {z : α} (hzCF : z ∈ C \ F.union) : z ∉ X

structure CircuitMatroid (α : Type u_1) : Type u_1

A matroid defined by circuit conditions.

• E : Set α

  The ground set

• CircuitPred : Set α → Prop

  The circuit predicate

• not_circuit_empty : ¬self.CircuitPred ∅

  Empty set is not a circuit

• circuit_not_subset : ∀ ⦃C C' : Set α⦄, self.CircuitPred C → self.CircuitPred C' → ¬C' ⊂ C

  No circuit is a subset of another circuit

• circuit_c3 : ∀ ⦃X C : Set α⦄ (F : ValidXFamily self.CircuitPred C X), ∀ z ∈ C \ F.union, ∃ (C' : Set α), self.CircuitPred C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ F.union) \ X

  Condition (C3) from Bruhn et al.

• circuit_maximal : ∀ X ⊆ self.E, Matroid.ExistsMaximalSubsetProperty (CircPredToIndep self.CircuitPred self.E) X

  Corresponding family of independent sets satisfies has the maximal subset property

• subset_ground : ∀ (C : Set α), self.CircuitPred C → C ⊆ self.E

  Every circuit is a subset of the ground set

theorem CircuitMatroid.not_circuit_empty {α : Type u_1} (self : CircuitMatroid α) : ¬self.CircuitPred ∅

Empty set is not a circuit

theorem CircuitMatroid.circuit_not_subset {α : Type u_1} (self : CircuitMatroid α) ⦃C : Set α⦄ ⦃C' : Set α⦄ : self.CircuitPred C → self.CircuitPred C' → ¬C' ⊂ C

No circuit is a subset of another circuit

theorem CircuitMatroid.circuit_c3 {α : Type u_1} (self : CircuitMatroid α) ⦃X : Set α⦄ ⦃C : Set α⦄ (F : ValidXFamily self.CircuitPred C X) (z : α) : z ∈ C \ F.union → ∃ (C' : Set α), self.CircuitPred C' ∧ z ∈ C' ∧ C' ⊆ (C ∪ F.union) \ X

Condition (C3) from Bruhn et al.

theorem CircuitMatroid.circuit_maximal {α : Type u_1} (self : CircuitMatroid α) (X : Set α) : X ⊆ self.E → Matroid.ExistsMaximalSubsetProperty (CircPredToIndep self.CircuitPred self.E) X

Corresponding family of independent sets satisfies has the maximal subset property

theorem CircuitMatroid.subset_ground {α : Type u_1} (self : CircuitMatroid α) (C : Set α) : self.CircuitPred C → C ⊆ self.E

Every circuit is a subset of the ground set

def CircuitMatroid.isIndep {α : Type u_1} (M : CircuitMatroid α) : Set α → Prop

Independence predicate in circuit matroid construction.

Equations

• M.isIndep = CircPredToIndep M.CircuitPred M.E

theorem CircuitMatroid.isIndep_empty {α : Type u_1} (M : CircuitMatroid α) : M.isIndep ∅

Empty set is independent in circuit matroid construction.

theorem CircuitMatroid.isIndep_subset {α : Type u_1} {I : Set α} {J : Set α} (M : CircuitMatroid α) (hI : M.isIndep I) (hJI : J ⊆ I) : M.isIndep J

Subset of independent set is independent in circuit matroid construction.

theorem CircuitMatroid.Maximal_iff {α : Type u_1} (M : CircuitMatroid α) (B : Set α) : Maximal (fun (K : Set α) => M.isIndep K ∧ K ⊆ M.E) B ↔ Maximal M.isIndep B

theorem nmem_insert {α : Type u_1} {z : α} {x : α} {I : Set α} (hx : z ≠ x) (hI : z ∉ I) : z ∉ x ᕃ I

theorem CircuitMatroid.isIndep_aug {α : Type u_1} {I : Set α} {I' : Set α} (M : CircuitMatroid α) (hI : M.isIndep I) (hMI : ¬Maximal M.isIndep I) (hMI' : Maximal M.isIndep I') : ∃ x ∈ I' \ I, M.isIndep (x ᕃ I)

def CircuitMatroid.IndepMatroid {α : Type u_1} (M : CircuitMatroid α) : IndepMatroid α

IndepMatroid corresponding to circuit matroid.

Equations

• M.IndepMatroid = { E := M.E, Indep := M.isIndep, indep_empty := ⋯, indep_subset := ⋯, indep_aug := ⋯, indep_maximal := ⋯, subset_ground := ⋯ }

def CircuitMatroid.matroid {α : Type u_1} (M : CircuitMatroid α) : Matroid α

Circuit matroid converted to Matroid.

Equations

• M.matroid = M.IndepMatroid.matroid