Documentation

Matroid.Rank.Nat

source
noncomputable def Matroid.rk {α : Type u_1} (M : Matroid α) (X : Set α) :
ℕ

The ℕ-valued rank function, taking a junk value of zero for infinite-rank sets. Intended to be used in a RankFinite matroid, or when the argument is known to be IsRkFinite. Otherwise Matroid.eRk is better.

Equations
Instances For
    source
    @[reducible]
    noncomputable def Matroid.rank {α : Type u_1} (M : Matroid α) :
    ℕ

    The ℕ-valued rank of the ground set of a matroid. Has a junk value of 0 for infinite-rank matroids.

    Equations
    Instances For
      source
      theorem Matroid.rank_def {α : Type u_1} (M : Matroid α) :
      M.rank = M.rk M.E
      source
      @[simp]
      theorem Matroid.eRk_toNat_eq_rk {α : Type u_1} (M : Matroid α) (X : Set α) :
      (M.eRk X).toNat = M.rk X
      source
      theorem Matroid.IsBase.ncard {α : Type u_1} {M : Matroid α} {B : Set α} (hB : M.IsBase B) :
      B.ncard = M.rank
      source
      theorem Matroid.IsRkFinite.cast_rk_eq {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.IsRkFinite X) :
      ↑(M.rk X) = M.eRk X
      source
      theorem Matroid.rk_eq_zero_of_not_isRkFinite {α : Type u_1} {M : Matroid α} {X : Set α} (hX : ¬M.IsRkFinite X) :
      M.rk X = 0
      source
      theorem Matroid.cast_rk_eq_eRk_of_finite {α : Type u_1} {X : Set α} (M : Matroid α) (hX : X.Finite) :
      ↑(M.rk X) = M.eRk X
      source
      theorem Matroid.Finset.cast_rk_eq {α : Type u_1} (M : Matroid α) (X : Finset α) :
      ↑(M.rk ↑X) = M.eRk ↑X
      source
      @[simp]
      theorem Matroid.cast_rk_eq {α : Type u_1} (M : Matroid α) [M.RankFinite] (X : Set α) :
      ↑(M.rk X) = M.eRk X
      source
      @[simp]
      theorem Matroid.cast_rank_eq {α : Type u_1} (M : Matroid α) [M.RankFinite] :
      ↑M.rank = M.eRank
      source
      theorem Matroid.rk_eq_of_eRk_eq {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.eRk X = M.eRk Y) :
      M.rk X = M.rk Y
      source
      theorem Matroid.IsRkFinite.eRk_eq_eRk_iff {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : M.IsRkFinite X) (hY : M.IsRkFinite Y) :
      M.eRk X = M.eRk Y ↔ M.rk X = M.rk Y
      source
      theorem Matroid.IsRkFinite.eRk_le_eRk_iff {α : Type u_1} {M : Matroid α} {X Y : Set α} (hX : M.IsRkFinite X) (hY : M.IsRkFinite Y) :
      M.eRk X ≤ M.eRk Y ↔ M.rk X ≤ M.rk Y
      source
      @[simp]
      theorem Matroid.eRk_eq_eRk_iff {α : Type u_1} {M : Matroid α} {X Y : Set α} [M.RankFinite] :
      M.eRk X = M.eRk Y ↔ M.rk X = M.rk Y
      source
      @[simp]
      theorem Matroid.eRk_le_eRk_iff {α : Type u_1} {M : Matroid α} {X Y : Set α} [M.RankFinite] :
      M.eRk X ≤ M.eRk Y ↔ M.rk X ≤ M.rk Y
      source
      @[simp]
      theorem Matroid.eRk_eq_coe_iff {α : Type u_1} {M : Matroid α} {X : Set α} [M.RankFinite] {n : ℕ} :
      M.eRk X = ↑n ↔ M.rk X = n
      source
      @[simp]
      theorem Matroid.eRk_le_coe_iff {α : Type u_1} {M : Matroid α} {X : Set α} [M.RankFinite] {n : ℕ} :
      M.eRk X ≤ ↑n ↔ M.rk X ≤ n
      source
      @[simp]
      theorem Matroid.coe_le_eRk_iff {α : Type u_1} {M : Matroid α} {X : Set α} [M.RankFinite] {n : ℕ} :
      ↑n ≤ M.eRk X ↔ n ≤ M.rk X
      source
      theorem Matroid.IsRkFinite.rk_le_rk_of_eRk_le_eRk {α : Type u_1} {M : Matroid α} {X Y : Set α} (hY : M.IsRkFinite Y) (hle : M.eRk X ≤ M.eRk Y) :
      M.rk X ≤ M.rk Y
      source
      @[simp]
      theorem Matroid.rk_ground {α : Type u_1} (M : Matroid α) :
      M.rk M.E = M.rank
      source
      @[simp]
      theorem Matroid.rk_inter_ground {α : Type u_1} (M : Matroid α) (X : Set α) :
      M.rk (X ∩ M.E) = M.rk X
      source
      @[simp]
      theorem Matroid.rk_ground_inter {α : Type u_1} (M : Matroid α) (X : Set α) :
      M.rk (M.E ∩ X) = M.rk X
      source
      @[simp]
      theorem Matroid.rk_union_ground {α : Type u_1} (M : Matroid α) (X : Set α) :
      M.rk (X ∪ M.E) = M.rank
      source
      @[simp]
      theorem Matroid.rk_ground_union {α : Type u_1} (M : Matroid α) (X : Set α) :
      M.rk (M.E ∪ X) = M.rank
      source
      theorem Matroid.rk_insert_of_notMem_ground {α : Type u_1} {M : Matroid α} {e : α} (X : Set α) (he : e ∉ M.E) :
      M.rk (insert e X) = M.rk X
      source
      theorem Matroid.rk_compl_union_of_disjoint {α : Type u_1} {X Y : Set α} (M : Matroid α) (hXY : Disjoint X Y) :
      M.rk (M.E \ X ∪ Y) = M.rk (M.E \ X)
      source
      theorem Matroid.le_rk_iff {α : Type u_1} {M : Matroid α} {X : Set α} [M.RankFinite] {n : ℕ} :
      n ≤ M.rk X ↔ ∃ I ⊆ X, M.Indep I ∧ I.ncard = n
      source
      theorem Matroid.rk_le_iff {α : Type u_1} {M : Matroid α} {X : Set α} [M.RankFinite] {n : ℕ} :
      M.rk X ≤ n ↔ ∀ {I : Set α}, I ⊆ X → M.Indep I → I.ncard ≤ n
      source
      theorem Matroid.rk_mono {α : Type u_1} (M : Matroid α) [M.RankFinite] :
      Monotone M.rk
      source
      theorem Matroid.IsRkFinite.rk_le_of_subset {α : Type u_1} {M : Matroid α} {X Y : Set α} (hY : M.IsRkFinite Y) (hXY : X ⊆ Y) :
      M.rk X ≤ M.rk Y
      source
      theorem Matroid.rk_le_of_subset {α : Type u_1} {X Y : Set α} (M : Matroid α) [M.RankFinite] (hXY : X ⊆ Y) :
      M.rk X ≤ M.rk Y
      source
      @[simp]
      theorem Matroid.rk_empty {α : Type u_1} (M : Matroid α) :
      M.rk ∅ = 0
      source
      @[simp]
      theorem Matroid.rk_closure_eq {α : Type u_1} {X : Set α} (M : Matroid α) :
      M.rk (M.closure X) = M.rk X
      source
      theorem Matroid.rk_le_rank {α : Type u_1} (M : Matroid α) [M.RankFinite] (X : Set α) :
      M.rk X ≤ M.rank
      source
      theorem Matroid.rk_eq_rank {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.E ⊆ X) :
      M.rk X = M.rank
      source
      theorem Matroid.Indep.rk_eq_ncard {α : Type u_1} {M : Matroid α} {I : Set α} (hI : M.Indep I) :
      M.rk I = I.ncard
      source
      theorem Matroid.Indep.rk_eq_card {α : Type u_1} {M : Matroid α} {I : Finset α} (hI : M.Indep ↑I) :
      M.rk ↑I = I.card
      source
      theorem Matroid.rk_le_card {α : Type u_1} (M : Matroid α) [M.Finite] (X : Set α) (hX : X ⊆ M.E := by aesop_mat) :
      M.rk X ≤ X.ncard
      source
      theorem Matroid.Indep.ncard_le_rk_of_subset {α : Type u_1} {M : Matroid α} {I X : Set α} [M.RankFinite] (hI : M.Indep I) (h : I ⊆ X) :
      I.ncard ≤ M.rk X
      source
      theorem Matroid.Indep.ncard_le_rank {α : Type u_1} {M : Matroid α} {I : Set α} [M.RankFinite] (hI : M.Indep I) :
      I.ncard ≤ M.rank
      source
      theorem Matroid.Indep.isBase_of_ncard {α : Type u_1} {M : Matroid α} {I : Set α} [M.RankFinite] (hI : M.Indep I) (hIcard : M.rank ≤ I.ncard) :
      M.IsBase I
      source
      theorem Matroid.Indep.isBase_of_card {α : Type u_1} {M : Matroid α} [M.RankFinite] {I : Finset α} (hI : M.Indep ↑I) (hIcard : M.rank ≤ I.card) :
      M.IsBase ↑I
      source
      theorem Matroid.IsBasis'.card {α : Type u_1} {M : Matroid α} {I X : Set α} (h : M.IsBasis' I X) :
      I.ncard = M.rk X
      source
      theorem Matroid.IsBasis'.rk_eq_rk {α : Type u_1} {M : Matroid α} {I X : Set α} (h : M.IsBasis' I X) :
      M.rk I = M.rk X
      source
      theorem Matroid.IsBasis.ncard_eq_rk {α : Type u_1} {M : Matroid α} {I X : Set α} (h : M.IsBasis I X) :
      I.ncard = M.rk X
      source
      theorem Matroid.IsBasis.finset_card {α : Type u_1} {M : Matroid α} {X : Set α} {I : Finset α} (hIX : M.IsBasis (↑I) X) :
      I.card = M.rk X
      source
      theorem Matroid.IsBasis'.finset_card {α : Type u_1} {M : Matroid α} {X : Set α} {I : Finset α} (hIX : M.IsBasis' (↑I) X) :
      I.card = M.rk X
      source
      theorem Matroid.IsBase.finset_card {α : Type u_1} {M : Matroid α} {B : Finset α} (hB : M.IsBase ↑B) :
      B.card = M.rank
      source
      theorem Matroid.rk_le_toFinset_card {α : Type u_1} (M : Matroid α) {X : Set α} (hX : X.Finite) :
      M.rk X ≤ hX.toFinset.card
      source
      theorem Matroid.rk_le_finset_card {α : Type u_1} (M : Matroid α) (X : Finset α) :
      M.rk ↑X ≤ X.card
      source
      theorem Matroid.rk_singleton_le {α : Type u_1} (M : Matroid α) (e : α) :
      M.rk {e} ≤ 1
      source
      theorem Matroid.IsBasis.rk_eq_rk {α : Type u_1} {M : Matroid α} {I X : Set α} (h : M.IsBasis I X) :
      M.rk I = M.rk X
      source
      theorem Matroid.rk_eq_zero_iff {α : Type u_1} {M : Matroid α} {X : Set α} [M.RankFinite] (hX : X ⊆ M.E) :
      M.rk X = 0 ↔ X ⊆ M.loops
      source
      @[simp]
      theorem Matroid.rk_loops {α : Type u_1} (M : Matroid α) :
      M.rk M.loops = 0
      source
      theorem Matroid.IsNonloop.rk_eq {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsNonloop e) :
      M.rk {e} = 1
      source
      theorem Matroid.IsLoop.rk_eq {α : Type u_1} {M : Matroid α} {e : α} (he : M.IsLoop e) :
      M.rk {e} = 0
      source
      theorem Matroid.IsCircuit.rk_add_one_eq {α : Type u_1} {M : Matroid α} {C : Finset α} (hC : M.IsCircuit ↑C) :
      M.rk ↑C + 1 = C.card
      source
      theorem Matroid.IsRkFinite.submod {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.IsRkFinite X) (Y : Set α) :
      M.rk (X ∩ Y) + M.rk (X ∪ Y) ≤ M.rk X + M.rk Y

      The ℕ-valued rank function is submodular. Due to junk values, we only need that X is finite-rank.

      source
      theorem Matroid.IsRkFinite.submod_right {α : Type u_1} {M : Matroid α} {Y : Set α} (hY : M.IsRkFinite Y) (X : Set α) :
      M.rk (X ∩ Y) + M.rk (X ∪ Y) ≤ M.rk X + M.rk Y
      source
      theorem Matroid.rk_submod {α : Type u_1} (M : Matroid α) [M.RankFinite] (X Y : Set α) :
      M.rk (X ∩ Y) + M.rk (X ∪ Y) ≤ M.rk X + M.rk Y
      source
      theorem Matroid.rk_submod_insert {α : Type u_1} {e : α} (M : Matroid α) [M.RankFinite] (X Y : Set α) :
      M.rk (insert e (X ∩ Y)) + M.rk (insert e (X ∪ Y)) ≤ M.rk (insert e X) + M.rk (insert e Y)
      source
      theorem Matroid.rk_submod_compl {α : Type u_1} (M : Matroid α) [M.RankFinite] (X Y : Set α) :
      M.rk (M.E \ (X ∪ Y)) + M.rk (M.E \ (X ∩ Y)) ≤ M.rk (M.E \ X) + M.rk (M.E \ Y)
      source
      theorem Matroid.rk_submod_insert_compl {α : Type u_1} {e : α} (M : Matroid α) [M.RankFinite] (X Y : Set α) :
      M.rk (M.E \ insert e (X ∪ Y)) + M.rk (M.E \ insert e (X ∩ Y)) ≤ M.rk (M.E \ insert e X) + M.rk (M.E \ insert e Y)
      source
      theorem Matroid.Indep.exists_insert_of_ncard_lt {α : Type u_1} {M : Matroid α} {I : Set α} [M.RankFinite] {J : Set α} (hI : M.Indep I) (hJ : M.Indep J) (hcard : I.ncard < J.ncard) :
      ∃ e ∈ J \ I, M.Indep (insert e I)
      source
      @[simp]
      theorem Matroid.rank_map {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : α → β) (hf : Set.InjOn f M.E) :
      (M.map f hf).rank = M.rank
      source
      theorem Matroid.rk_union_le_rk_add_rk {α : Type u_1} (M : Matroid α) (X Y : Set α) :
      M.rk (X ∪ Y) ≤ M.rk X + M.rk Y
      source
      theorem Matroid.ext_rk {α : Type u_1} {M N : Matroid α} [M.RankFinite] [N.RankFinite] (hE : M.E = N.E) (h : ∀ X ⊆ M.E, M.rk X = N.rk X) :
      M = N
      source
      @[simp]
      theorem Matroid.rank_eq_zero_iff {α : Type u_1} {M : Matroid α} [M.RankFinite] :
      M.rank = 0 ↔ M = loopyOn M.E
      source
      theorem Matroid.exists_of_rank_eq_zero {α : Type u_1} {M : Matroid α} [M.RankFinite] (h : M.rank = 0) :
      ∃ (E : Set α), M = loopyOn E
      source
      @[simp]
      theorem Matroid.range_rk_bddAbove {α : Type u_1} (M : Matroid α) [M.RankFinite] :
      BddAbove (Set.range M.rk)
      source
      @[simp]
      theorem Matroid.range_rk_finite {α : Type u_1} (M : Matroid α) [M.RankFinite] :
      (Set.range M.rk).Finite