Theorems · Theorem · number theory

Finset.exists_subset_addSpan_card_le_of_forall_addDissociated

∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : DecidableEq α] [inst_2 : Fintype α] {s : Finset α} {d : ℕ},
  (∀ s' ⊆ s, AddDissociated ↑s' → s'.card ≤ d) → ∃ s' ⊆ s, s'.card ≤ d ∧ s ⊆ s'.addSpan

If every dissociated subset of s has size at most d, then s is actually generated by a subset of size at most d. This is a dissociation analog of the fact that a set whose linearly independent subspaces all have size at most d is of dimension at most d itself.

Defined in

Mathlib.Combinatorics.Additive.Dissociation

Cited by

0 results in Mathlib

Foundations

Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupDecidableEqFintype