structure CircuitMatroid (α : Type u) : Type u

A general infinite matroid as described by its circuits. Showing this definition actually corresponds to a matroid is TODO.

• E : Set α
• IsCircuit : Set α → Prop
• empty_not_isCircuit : ¬self.IsCircuit ∅
• circuit_antichain : IsAntichain (fun (x1 x2 : Set α) => x1 ⊆ x2) {C : Set α | self.IsCircuit C}
• elimination (ι : Type u) (x : ι → α) (I : ι → Set α) (J : Set α) (z : α) : (∀ (i : ι), self.IsCircuit (insert (x i) (I i))) → Function.Injective x → (∀ (i : ι), x i ∉ I i) → self.IsCircuit (J ∪ Set.range x) → (∀ (i : ι), z ∉ I i) → ∃ C ⊆ J ∪ ⋃ (i : ι), I i, self.IsCircuit C ∧ z ∈ C
• circuit_subset_ground ⦃C : Set α⦄ : self.IsCircuit C → C ⊆ self.E

structure FiniteCircuitMatroid (α : Type u_2) : Type u_2

A finitary matroid as described by its circuits.

• E : Set α
• IsCircuit : Set α → Prop
• empty_not_isCircuit : ¬self.IsCircuit ∅
• circuit_antichain : IsAntichain (fun (x1 x2 : Set α) => x1 ⊆ x2) {C : Set α | self.IsCircuit C}
• circuit_elimination ⦃C₁ C₂ : Set α⦄ ⦃e : α⦄ : self.IsCircuit C₁ → self.IsCircuit C₂ → C₁ ≠ C₂ → e ∈ C₁ → e ∈ C₂ → ∃ (C : Set α), self.IsCircuit C ∧ e ∉ C ∧ C ⊆ C₁ ∪ C₂
• circuit_finite ⦃C : Set α⦄ : self.IsCircuit C → C.Finite
• circuit_subset_ground ⦃C : Set α⦄ : self.IsCircuit C → C ⊆ self.E

structure FiniteCircuitMatroid.Indep {α : Type u_1} (M : FiniteCircuitMatroid α) (I : Set α) : Prop

• subset_ground : I ⊆ M.E
• not_isCircuit_of_subset ⦃C : Set α⦄ : C ⊆ I → ¬M.IsCircuit C

theorem FiniteCircuitMatroid.indep_iff {α : Type u_1} (M : FiniteCircuitMatroid α) (I : Set α) : M.Indep I ↔ I ⊆ M.E ∧ ∀ ⦃C : Set α⦄, C ⊆ I → ¬M.IsCircuit C

theorem FiniteCircuitMatroid.Indep.subset {α : Type u_1} {I J : Set α} {M : FiniteCircuitMatroid α} (hJ : M.Indep J) (hIJ : I ⊆ J) : M.Indep I

theorem FiniteCircuitMatroid.Indep.augment {α : Type u_1} {I : Set α} {M : FiniteCircuitMatroid α} {J : Set α} (hI : M.Indep I) (hIfin : I.Finite) (hJ : M.Indep J) (hJfin : J.Finite) (hIJ : I.ncard < J.ncard) : ∃ e ∈ J, e ∉ I ∧ M.Indep (insert e I)

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

The matroid of a FiniteCircuitMatroid.

Equations

• M.matroid = (IndepMatroid.ofFinitaryCardAugment M.E M.Indep ⋯ ⋯ ⋯ ⋯ ⋯).matroid

@[simp]

theorem FiniteCircuitMatroid.matroid_E {α : Type u_1} (M : FiniteCircuitMatroid α) : M.matroid.E = M.E

@[simp]

theorem FiniteCircuitMatroid.matroid_indep_iff {α : Type u_1} {I : Set α} {M : FiniteCircuitMatroid α} : M.matroid.Indep I ↔ I ⊆ M.E ∧ ∀ ⦃C : Set α⦄, C ⊆ I → ¬M.IsCircuit C

@[simp]

theorem FiniteCircuitMatroid.matroid_isCircuit {α : Type u_1} {M : FiniteCircuitMatroid α} : M.matroid.IsCircuit = M.IsCircuit

instance FiniteCircuitMatroid.instFinitaryMatroid {α : Type u_1} {M : FiniteCircuitMatroid α} : M.matroid.Finitary

def FiniteCircuitMatroid.ofNonspanningCircuit {α : Type u_1} (E : Set α) (IsNonspanningCircuit : Set α → Prop) (r : ℕ) (ground_set : ∀ (C : Set α), IsNonspanningCircuit C → C ⊆ E) (rank_not_spanning : ∀ (C : Set α), IsNonspanningCircuit C → C.Finite ∧ C.ncard ≤ r) (empty_not_isCircuit : ¬IsNonspanningCircuit ∅) (circuit_antichain : IsAntichain (fun (x1 x2 : Set α) => x1 ⊆ x2) {C : Set α | IsNonspanningCircuit C}) (circuit_elimination : ∀ ⦃C₁ C₂ : Set α⦄ ⦃e : α⦄, IsNonspanningCircuit C₁ → IsNonspanningCircuit C₂ → C₁ ≠ C₂ → e ∈ C₁ → e ∈ C₂ → ∃ (C : Set α), IsNonspanningCircuit C ∧ e ∉ C ∧ C ⊆ C₁ ∪ C₂) : FiniteCircuitMatroid α

Equations

• One or more equations did not get rendered due to their size.