structure Matroid.StronglyPreservable {α : Type u_1} (μ : Matroid α → Set α → ℕ∞) : Prop

• dual (M : Matroid α) (X : Set α) : μ M✶ X = μ M X
• inter_ground (M : Matroid α) (X : Set α) : μ M (X ∩ M.E) = μ M X
• delete_le (M : Matroid α) (X D : Set α) : μ (M.delete D) X ≤ μ M X
• base_preservable ⦃M : Matroid α⦄ ⦃B X : Set α⦄ ⦃k : ℕ∞⦄ : M.IsBase B → k ≤ μ M X → ∃ V ⊆ M.E, Disjoint V B ∧ V.encard ≤ k ∧ μ (M.restrict (B ∪ V)) X = k

theorem Matroid.stronglyPreservable_iff {α : Type u_1} (μ : Matroid α → Set α → ℕ∞) : StronglyPreservable μ ↔ (∀ (M : Matroid α) (X : Set α), μ M✶ X = μ M X) ∧ (∀ (M : Matroid α) (X : Set α), μ M (X ∩ M.E) = μ M X) ∧ (∀ (M : Matroid α) (X D : Set α), μ (M.delete D) X ≤ μ M X) ∧ ∀ ⦃M : Matroid α⦄ ⦃B X : Set α⦄ ⦃k : ℕ∞⦄, M.IsBase B → k ≤ μ M X → ∃ V ⊆ M.E, Disjoint V B ∧ V.encard ≤ k ∧ μ (M.restrict (B ∪ V)) X = k

theorem Matroid.StronglyPreservable.contract_le {α : Type u_1} {μ : Matroid α → Set α → ℕ∞} (hμ : StronglyPreservable μ) (M : Matroid α) (X C : Set α) : μ (M.contract C) X ≤ μ M X

theorem Matroid.StronglyPreservable.le_of_isMinor {α : Type u_1} {μ : Matroid α → Set α → ℕ∞} (hμ : StronglyPreservable μ) {M N : Matroid α} (h : N ≤m M) (X : Set α) : μ N X ≤ μ M X

theorem Matroid.StronglyPreservable.exists_preserve_eq {α : Type u_1} {M : Matroid α} {B X : Set α} {k : ℕ∞} {μ : Matroid α → Set α → ℕ∞} (hμ : StronglyPreservable μ) (hB : M.IsBase B) (hk : k ≤ μ M X) : ∃ (U : Set α) (V : Set α), U ⊆ B ∧ V ⊆ M.E ∧ Disjoint V B ∧ U.encard ≤ k ∧ V.encard ≤ k ∧ μ ((M.contract (B \ U)).delete ((M.E \ B) \ V)) X = k

theorem Matroid.StronglyPreservable.exists_preserve_le {α : Type u_1} {M : Matroid α} {B X : Set α} {k : ℕ∞} {μ : Matroid α → Set α → ℕ∞} (hμ : StronglyPreservable μ) (hB : M.IsBase B) (hk : k ≤ μ M X) : ∃ (U : Set α) (V : Set α), U ⊆ B ∧ V ⊆ M.E ∧ Disjoint V B ∧ U.encard ≤ k ∧ V.encard ≤ k ∧ ∀ C ⊆ B, ∀ D ⊆ M.E \ B, Disjoint C U → Disjoint D V → k ≤ μ ((M.contract C).delete D) X

theorem Matroid.StronglyPreservable.exists_finite_counterexample_of_lt_sum' {α : Type u_1} {ι : Type u_3} [Fintype ι] {μ : ι → Matroid α → Set α → ℕ∞} (hμ : ∀ (i : ι), StronglyPreservable (μ i)) (M : Matroid α) (g : Matroid α → ℕ∞) (hg : Monotone g) (X : ι → Set α) (h_lt : g M < ∑ i : ι, μ i M (X i)) : ∃ (N : Matroid α), N ≤m M ∧ N.Finite ∧ g N < ∑ i : ι, μ i N (X i)

theorem Matroid.StronglyPreservable.exists_finite_counterexample_of_lt_sum {α : Type u_1} {ι : Type u_3} [Fintype ι] {μ : Matroid α → Set α → ℕ∞} (hμ : StronglyPreservable μ) (M : Matroid α) (g : Matroid α → ℕ∞) (hg : Monotone g) (X : ι → Set α) (h_lt : g M < ∑ i : ι, μ M (X i)) : ∃ (N : Matroid α), N ≤m M ∧ N.Finite ∧ g N < ∑ i : ι, μ N (X i)

theorem Matroid.StronglyPreservable.exists_finite_counterexample_of_sum_lt_sum {α : Type u_1} {μ : Matroid α → Set α → ℕ∞} (hμ : StronglyPreservable μ) {ι : Type u_3} {η : Type u_4} [Fintype ι] [Fintype η] (M : Matroid α) (X : ι → Set α) (Y : η → Set α) (h_lt : ∑ i : ι, μ M (X i) < ∑ i : η, μ M (Y i)) : ∃ (N : Matroid α), N ≤m M ∧ N.Finite ∧ ∑ i : ι, μ N (X i) < ∑ i : η, μ N (Y i)