Documentation

Matroid.Triangle

structure Matroid.IsTriangle {α : Type u_2} (M : Matroid α) (T : Set α) :

A triangle is a three-element circuit.

isCircuit : M.IsCircuit T
three_elements : T.encard = 3

Instances For

theorem Matroid.isTriangle_iff {α : Type u_2} (M : Matroid α) (T : Set α) :

M.IsTriangle T ↔ M.IsCircuit T ∧ T.encard = 3

instance Matroid.instGroundedPredSetIsTriangle :

GroundedPred fun {α : Type u_3} => IsTriangle

instance Matroid.instInvariantFunSetPropIsTriangle :

InvariantFun (fun {α : Type u_3} => IsTriangle) fun {β : Type u_4} => IsTriangle

def Matroid.IsTriad {α : Type u_2} (M : Matroid α) (T : Set α) :

A triad is a three-element cocircuit

Equations

M.IsTriad T = M✶.IsTriangle T

Instances For

instance Matroid.instGroundedPredSetIsTriad :

GroundedPred fun {α : Type u_3} => IsTriad

instance Matroid.instInvariantFunSetPropIsTriad :

InvariantFun (fun {α : Type u_3} => IsTriad) fun {β : Type u_4} => IsTriad

theorem Matroid.isTriad_iff {α : Type u_2} {T : Set α} {M : Matroid α} :

M.IsTriad T ↔ M.IsCocircuit T ∧ T.encard = 3

theorem Matroid.IsTriad.isCocircuit {α : Type u_2} {T : Set α} {M : Matroid α} (h : M.IsTriad T) :

M.IsCocircuit T

theorem Matroid.IsTriangle.subset_ground {α : Type u_2} {T : Set α} {M : Matroid α} (hT : M.IsTriangle T) :

T ⊆ M.E

theorem Matroid.IsTriad.subset_ground {α : Type u_2} {T : Set α} {M : Matroid α} (hT : M.IsTriad T) :

T ⊆ M.E

theorem Matroid.IsTriangle.dual_isTriad {α : Type u_2} {T : Set α} {M : Matroid α} (h : M.IsTriangle T) :

theorem Matroid.IsTriad.dual_isTriangle {α : Type u_2} {T : Set α} {M : Matroid α} (h : M.IsTriad T) :

M✶.IsTriangle T

@[simp]

theorem Matroid.dual_isTriad_iff {α : Type u_2} {T : Set α} {M : Matroid α} :

M✶.IsTriad T ↔ M.IsTriangle T

@[simp]

theorem Matroid.dual_isTriangle_iff {α : Type u_2} {T : Set α} {M : Matroid α} :

M✶.IsTriangle T ↔ M.IsTriad T

@[simp]

theorem Matroid.bDual_isTriad_iff {b : Bool} {α : Type u_2} {X : Set α} {M : Matroid α} :

(M.bDual b).IsTriad X ↔ (M.bDual !b).IsTriangle X

theorem Matroid.IsTriangle.nonempty {α : Type u_2} {T : Set α} {M : Matroid α} (h : M.IsTriangle T) :

theorem Matroid.IsTriangle.nontrivial_diff_singleton {α : Type u_2} {T : Set α} {M : Matroid α} (h : M.IsTriangle T) (e : α) :

(T \ {e}).Nontrivial

theorem Matroid.IsTriangle.nontrivial {α : Type u_2} {T : Set α} {M : Matroid α} (h : M.IsTriangle T) :

theorem Matroid.IsTriangle.finite {α : Type u_2} {T : Set α} {M : Matroid α} (h : M.IsTriangle T) :

theorem Matroid.IsTriangle.ne₁₂ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

e ≠ f

theorem Matroid.IsTriangle.ne₁₃ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

e ≠ g

theorem Matroid.IsTriangle.ne₂₃ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

f ≠ g

theorem Matroid.IsTriangle.nodup {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

[e, f, g].Nodup

theorem Matroid.IsTriangle.swap_right {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

M.IsTriangle {e, g, f}

theorem Matroid.IsTriangle.rotate {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

M.IsTriangle {g, e, f}

theorem Matroid.IsTriangle.rotate_left {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

M.IsTriangle {f, g, e}

theorem Matroid.IsTriangle.swap_left {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

M.IsTriangle {f, e, g}

theorem Matroid.IsTriangle.reverse {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

M.IsTriangle {g, f, e}

theorem Matroid.IsTriad.swap_right {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriad {e, f, g}) :

M.IsTriad {e, g, f}

theorem Matroid.IsTriad.rotate {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriad {e, f, g}) :

M.IsTriad {g, e, f}

theorem Matroid.IsTriad.rotate_left {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriad {e, f, g}) :

M.IsTriad {f, g, e}

theorem Matroid.IsTriad.swap_left {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriad {e, f, g}) :

M.IsTriad {f, e, g}

theorem Matroid.IsTriad.reverse {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriad {e, f, g}) :

M.IsTriad {g, f, e}

theorem Matroid.IsTriangle.indep₁₂ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

theorem Matroid.IsTriangle.indep₁₃ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

theorem Matroid.IsTriangle.indep₂₃ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

theorem Matroid.IsTriangle.mem_ground₁ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

e ∈ M.E

theorem Matroid.IsTriangle.mem_ground₂ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

f ∈ M.E

theorem Matroid.IsTriangle.mem_ground₃ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

g ∈ M.E

theorem Matroid.IsTriangle.mem_closure₁ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

e ∈ M.closure {f, g}

theorem Matroid.IsTriangle.mem_closure₂ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

f ∈ M.closure {e, g}

theorem Matroid.IsTriangle.mem_closure₃ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

g ∈ M.closure {e, f}

theorem Matroid.IsTriangle.isNonloop_of_mem {α : Type u_2} {e : α} {T : Set α} {M : Matroid α} (h : M.IsTriangle T) (heT : e ∈ T) :

theorem Matroid.IsTriangle.isNonloop₁ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

theorem Matroid.IsTriangle.isNonloop₂ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

theorem Matroid.IsTriangle.isNonloop₃ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

theorem Matroid.IsTriangle.isNonloop_bDual_of_mem {α : Type u_2} {e : α} {T : Set α} {M : Matroid α} (h : M.IsTriangle T) (heT : e ∈ T) {b : Bool} :

(M.bDual b).IsNonloop e

theorem Matroid.IsTriangle.isNonloop_of_mem_of_bDual {b : Bool} {α : Type u_2} {e : α} {T : Set α} {M : Matroid α} (h : (M.bDual b).IsTriangle T) (heT : e ∈ T) :

theorem Matroid.IsTriangle.isNonloop_of_bDual₁ {b : Bool} {α : Type u_2} {e f g : α} {M : Matroid α} (h : (M.bDual b).IsTriangle {e, f, g}) :

theorem Matroid.IsTriangle.isNonloop_of_bDual₂ {b : Bool} {α : Type u_2} {e f g : α} {M : Matroid α} (h : (M.bDual b).IsTriangle {e, f, g}) :

theorem Matroid.IsTriangle.isNonloop_of_bDual₃ {b : Bool} {α : Type u_2} {e f g : α} {M : Matroid α} (h : (M.bDual b).IsTriangle {e, f, g}) :

theorem Matroid.IsTriangle.isNonloop_bDual₁ {b : Bool} {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

(M.bDual b).IsNonloop e

theorem Matroid.IsTriangle.isNonloop_bDual₂ {b : Bool} {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

(M.bDual b).IsNonloop f

theorem Matroid.IsTriangle.isNonloop_bDual₃ {b : Bool} {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

(M.bDual b).IsNonloop g

theorem Matroid.IsTriangle.isNonColoop_of_mem {α : Type u_2} {e : α} {T : Set α} {M : Matroid α} (h : M.IsTriangle T) (heT : e ∈ T) :

M.IsNonColoop e

theorem Matroid.IsTriangle.isNonColoop₁ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

M.IsNonColoop e

theorem Matroid.IsTriangle.isNonColoop₂ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

M.IsNonColoop f

theorem Matroid.IsTriangle.isNonColoop₃ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

M.IsNonColoop g

theorem Matroid.IsTriangle.notMem_of_mem_of_parallel {α : Type u_2} {e f : α} {T : Set α} {M : Matroid α} (h : M.IsTriangle T) (hef : M.Parallel e f) (heT : e ∈ T) (hne : e ≠ f) :

f ∉ T

theorem Matroid.IsTriangle.eq_of_parallel_mem_mem {α : Type u_2} {e f : α} {T : Set α} {M : Matroid α} (h : M.IsTriangle T) (hef : M.Parallel e f) (heT : e ∈ T) (hfT : f ∈ T) :

e = f

theorem Matroid.IsTriangle.parallel_contract₁ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

(M.contract {e}).Parallel f g

theorem Matroid.IsTriangle.parallel_contract₂ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

(M.contract {f}).Parallel e g

theorem Matroid.IsTriangle.parallel_contract₃ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) :

(M.contract {g}).Parallel e f

theorem Matroid.isTriangle_iff_parallel_contract {α : Type u_2} {e f : α} {M : Matroid α} {x : α} (hef : ¬M.Parallel e f) :

M.IsTriangle {e, f, x} ↔ (M.contract {x}).Parallel e f

theorem Matroid.IsTriangle.restrict_simple {α : Type u_2} {T : Set α} {M : Matroid α} (hT : M.IsTriangle T) :

(M.restrict T).Simple

@[simp]

theorem Matroid.not_isTriangle_pair {α : Type u_2} (M : Matroid α) (e f : α) :

¬M.IsTriangle {e, f}

theorem Matroid.IsTriad.mem_ground₁ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriad {e, f, g}) :

e ∈ M.E

theorem Matroid.IsTriad.mem_ground₂ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriad {e, f, g}) :

f ∈ M.E

theorem Matroid.IsTriad.mem_ground₃ {α : Type u_2} {e f g : α} {M : Matroid α} (h : M.IsTriad {e, f, g}) :

g ∈ M.E

theorem Matroid.IsTriangle.eRk {α : Type u_2} {T : Set α} {M : Matroid α} (hT : M.IsTriangle T) :

M.eRk T = 2

theorem Matroid.IsTriad.eRk_dual {α : Type u_2} {T : Set α} {M : Matroid α} (hT : M.IsTriad T) :

M✶.eRk T = 2

theorem Matroid.IsTriangle.eRelRk {α : Type u_2} {e : α} {T : Set α} {M : Matroid α} (hT : M.IsTriangle T) (he : e ∈ T) :

M.eRelRk {e} T = 1

theorem Matroid.IsTriangle.eRk_union_le {α : Type u_2} {T X : Set α} {M : Matroid α} (hT : M.IsTriangle T) (hTX : (X ∩ T).Nonempty) :

M.eRk (T ∪ X) ≤ M.eRk X + 1

theorem Matroid.isTriangle_triple_of_dep {α : Type u_2} {M : Matroid α} {e f g : α} (hT : M.Dep {e, f, g}) (he : M.IsNonloop e) (hf : M.IsNonloop f) (hg : M.IsNonloop g) (hef : ¬M.Parallel e f) (heg : ¬M.Parallel e g) (hfg : ¬M.Parallel f g) :

M.IsTriangle {e, f, g}

theorem Matroid.isTriangle_of_dep_of_encard_le {α : Type u_2} {T : Set α} {M : Matroid α} [h : M.Simple] (hT : M.Dep T) (hcard : T.encard ≤ 3) :

structure Matroid.Triassic {α : Type u_2} (M : Matroid α) :

forall_mem_triangle (e : α) : e ∈ M.E → ∃ (T : Set α), M.IsTriangle T ∧ e ∈ T
forall_mem_triad (e : α) : e ∈ M.E → ∃ (T : Set α), M.IsTriad T ∧ e ∈ T

Instances For

theorem Matroid.triassic_iff {α : Type u_2} (M : Matroid α) :

M.Triassic ↔ (∀ e ∈ M.E, ∃ (T : Set α), M.IsTriangle T ∧ e ∈ T) ∧ ∀ e ∈ M.E, ∃ (T : Set α), M.IsTriad T ∧ e ∈ T

@[simp]

theorem Matroid.triassic_dual_iff {α : Type u_2} {M : Matroid α} :

M✶.Triassic ↔ M.Triassic

theorem Matroid.Triassic.dual {α : Type u_2} {M : Matroid α} :

M.Triassic → M✶.Triassic

Alias of the reverse direction of Matroid.triassic_dual_iff.

theorem Matroid.triassic_iff_forall_bool {α : Type u_2} {M : Matroid α} :

M.Triassic ↔ ∀ (b : Bool), ∀ e ∈ M.E, ∃ (T : Set α), (M.bDual b).IsTriangle T ∧ e ∈ T

theorem Matroid.Triassic.mem_triangle_bDual {α : Type u_2} {e : α} {M : Matroid α} (hM : M.Triassic) (he : e ∈ M.E) (b : Bool) :

∃ (T : Set α), (M.bDual b).IsTriangle T ∧ e ∈ T

theorem Matroid.Triassic.exists_triangle_bDual {α : Type u_2} {e : α} {M : Matroid α} (hM : M.Triassic) (he : e ∈ M.E) (b : Bool) :

∃ (x : α) (y : α), (M.bDual b).IsTriangle {e, x, y}

theorem Matroid.IsTriangle.mem_iff_mem_of_isCocircuit {α : Type u_2} {e f g : α} {K : Set α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) (hK : M.IsCocircuit K) (heK : e ∉ K) :

f ∈ K ↔ g ∈ K

theorem Matroid.IsTriad.mem_iff_mem_of_isCircuit {α : Type u_2} {e f g : α} {C : Set α} {M : Matroid α} (h : M.IsTriad {e, f, g}) (hC : M.IsCircuit C) (heC : e ∉ C) :

f ∈ C ↔ g ∈ C

theorem Matroid.IsTriangle.mem_or_mem_of_isCocircuit {α : Type u_2} {e f g : α} {K : Set α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) (hK : M.IsCocircuit K) (heK : e ∈ K) :

f ∈ K ∨ g ∈ K

theorem Matroid.IsTriangle.mem_of_mem_of_notMem_of_is_Cocircuit {α : Type u_2} {e f g : α} {K : Set α} {M : Matroid α} (h : M.IsTriangle {e, f, g}) (hK : M.IsCocircuit K) (heK : e ∈ K) (hfK : f ∉ K) :

g ∈ K

theorem Matroid.IsTriangle.mem_or_mem_of_isCircuit_bDual {b : Bool} {α : Type u_2} {e f g : α} {K : Set α} {M : Matroid α} (h : (M.bDual b).IsTriangle {e, f, g}) (hK : (M.bDual !b).IsCircuit K) (heK : e ∈ K) :

f ∈ K ∨ g ∈ K

theorem Matroid.IsTriangle.mem_iff_mem_of_isCircuit_bDual {b : Bool} {α : Type u_2} {e f g : α} {K : Set α} {M : Matroid α} (h : (M.bDual b).IsTriangle {e, f, g}) (hK : (M.bDual !b).IsCircuit K) (heK : e ∉ K) :

f ∈ K ↔ g ∈ K

theorem Matroid.IsTriangle.mem_of_mem_of_notMem_of_isCircuit_bDual {α : Type u_2} {e f g : α} {K : Set α} {M : Matroid α} {b : Bool} (h : (M.bDual b).IsTriangle {e, f, g}) (hK : (M.bDual !b).IsCircuit K) (heK : e ∈ K) (hfK : f ∉ K) :

g ∈ K

theorem Matroid.IsTriangle.eq_of_isTriad {α : Type u_2} {e f g : α} {M : Matroid α} {x y : α} (h : M.IsTriangle {e, f, g}) (h' : M.IsTriad {e, x, y}) :

f = x ∨ f = y ∨ g = x ∨ g = y

theorem Matroid.IsFiniteRankUniform.isTriangle_iff {α : Type u_2} {C : Set α} {M : Matroid α} (hM : M.IsFiniteRankUniform 2) :

M.IsTriangle C ↔ C.encard = 3 ∧ C ⊆ M.E

theorem Matroid.isTriangle_restrict_iff {α : Type u_2} {T : Set α} {M : Matroid α} {R : Set α} :

(M.restrict R).IsTriangle T ↔ M.IsTriangle T ∧ T ⊆ R

theorem Matroid.IsTriangle.restrict {α : Type u_2} {T : Set α} {M : Matroid α} {R : Set α} (hT : M.IsTriangle T) (hTR : T ⊆ R) :

(M.restrict R).IsTriangle T

@[simp]

theorem Matroid.isTriangle_delete_iff {α : Type u_2} {T : Set α} {M : Matroid α} {D : Set α} :

(M.delete D).IsTriangle T ↔ M.IsTriangle T ∧ Disjoint T D

@[simp]

theorem Matroid.isTriad_contract_iff {α : Type u_2} {T : Set α} {M : Matroid α} {C : Set α} :

(M.contract C).IsTriad T ↔ M.IsTriad T ∧ Disjoint T C

theorem Matroid.Simple.contractElem_simple_of_notMem_triangle {α : Type u_2} {e : α} {M : Matroid α} (hM : M.Simple) (he : ∀ (T : Set α), M.IsTriangle T → e ∉ T) :

(M.contract {e}).Simple