theorem ENat.strong_induction_on {p : ℕ∞ → Prop} (n : ℕ∞) (h : ∀ (n : ℕ∞), (∀ m < n, p m) → p n) : p n

theorem ENat.nat_strong_induction_on {p : ℕ∞ → Prop} (n : ℕ∞) (htop : p ⊤) (h : ∀ (n : ℕ), (∀ m < n, p ↑m) → p ↑n) : p n

theorem Matroid.inter_iUnion_eq_of_pairwiseDisjoint_of_forall_subset {α : Type u_1} {ι : Type u_2} {s t : ι → Set α} (h : Pairwise (Function.onFun Disjoint t)) (hst : ∀ (i : ι), s i ⊆ t i) (i : ι) : t i ∩ ⋃ (j : ι), s j = s i

theorem Matroid.tsum_nullity_le {α : Type u_1} {ι : Type u_2} (M : Matroid α) {X : ι → Set α} (hX : Pairwise (Function.onFun Disjoint X)) : ∑' (i : ι), M.nullity (X i) ≤ M.nullity (⋃ (i : ι), X i)

theorem Matroid.IsSkewFamily.nullity_iUnion_eq {α : Type u_1} {ι : Type u_2} {M : Matroid α} {X : ι → Set α} (hX : M.IsSkewFamily X) (h : Pairwise (Function.onFun Disjoint X)) : M.nullity (⋃ (i : ι), X i) = ∑' (i : ι), M.nullity (X i)

theorem Matroid.Skew.nullity_union_eq {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXY : M.Skew X Y) (hdj : Disjoint X Y) : M.nullity (X ∪ Y) = M.nullity X + M.nullity Y

theorem Matroid.tsum_nullity_eq_nullity_iUnion_iff_isSkewFamily {α : Type u_1} {ι : Type u_2} {M : Matroid α} {X : ι → Set α} (hX : Pairwise (Function.onFun Disjoint X)) (hXE : ∀ (i : ι), X i ⊆ M.E) (hfin : M.nullity (⋃ (i : ι), X i) < ⊤) : M.nullity (⋃ (i : ι), X i) = ∑' (i : ι), M.nullity (X i) ↔ M.IsSkewFamily X

theorem Matroid.nullity_union_eq_iff {α : Type u_1} {M : Matroid α} {X Y : Set α} (hdj : Disjoint X Y) (hfin : M.nullity (X ∪ Y) ≠ ⊤) (hXE : X ⊆ M.E := by aesop_mat) (hYE : Y ⊆ M.E := by aesop_mat) : M.nullity (X ∪ Y) = M.nullity X + M.nullity Y ↔ M.Skew X Y

theorem Matroid.not_skew_iff_nullity_lt_nullity_project {α : Type u_1} {M : Matroid α} {X Y : Set α} (hfin : M.nullity Y ≠ ⊤) (hdj : Disjoint X Y) (hX : X ⊆ M.E := by aesop_mat) (hY : Y ⊆ M.E := by aesop_mat) : ¬M.Skew X Y ↔ M.nullity Y < (M.project X).nullity Y

theorem Matroid.not_skew_iff_nullity_union_gt {α : Type u_1} {M : Matroid α} {X Y : Set α} (hfin : M.nullity (X ∪ Y) ≠ ⊤) (hdj : Disjoint X Y) (hX : X ⊆ M.E := by aesop_mat) (hY : Y ⊆ M.E := by aesop_mat) : ¬M.Skew X Y ↔ M.nullity X + M.nullity Y < M.nullity (X ∪ Y)

theorem Matroid.nullity_biUnion_mono {α : Type u_1} {ι : Type u_2} {M : Matroid α} {X Y : ι → Set α} {I : Set ι} (hX : I.PairwiseDisjoint X) (hY : I.PairwiseDisjoint Y) (hn : ∀ i ∈ I, M.nullity (X i) ≤ M.nullity (Y i)) (hcl : ∀ i ∈ I, M.closure (X i) ⊆ M.closure (Y i)) : M.nullity (⋃ i ∈ I, X i) ≤ M.nullity (⋃ i ∈ I, Y i)

theorem Matroid.nullity_iUnion_mono {α : Type u_1} {ι : Type u_2} {M : Matroid α} {X Y : ι → Set α} (hX : Pairwise (Function.onFun Disjoint X)) (hY : Pairwise (Function.onFun Disjoint Y)) (hn : ∀ (i : ι), M.nullity (X i) ≤ M.nullity (Y i)) (hcl : ∀ (i : ι), M.closure (X i) ⊆ M.closure (Y i)) : M.nullity (⋃ (i : ι), X i) ≤ M.nullity (⋃ (i : ι), Y i)

theorem Matroid.nullity_iUnion_congr {α : Type u_1} {ι : Type u_2} {M : Matroid α} {X Y : ι → Set α} (hX : Pairwise (Function.onFun Disjoint X)) (hY : Pairwise (Function.onFun Disjoint Y)) (hn : ∀ (i : ι), M.nullity (X i) = M.nullity (Y i)) (hcl : ∀ (i : ι), M.closure (X i) = M.closure (Y i)) : M.nullity (⋃ (i : ι), X i) = M.nullity (⋃ (i : ι), Y i)