English
If every dissociated subset of s has size at most d, then there exists a subset s' ⊆ s with |s'| ≤ d such that s ⊆ mulSpan(s').
Русский
Если каждая диссоциированная подмножество s имеет размер не более d, тогда существует подмножество s' ⊆ s такое, что |s'| ≤ d и s ⊆ mulSpan(s').
LaTeX
$$$\exists s' \subseteq s, \ |s'| \le d \ \land\ s \subseteq mulSpan(s')$$$
Lean4
/-- 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 subsets all have
size at most `d` is of dimension at most `d` itself. -/
@[to_additive /-- 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. -/
]
theorem exists_subset_mulSpan_card_le_of_forall_mulDissociated
(hs : ∀ s', s' ⊆ s → MulDissociated (s' : Set α) → s'.card ≤ d) : ∃ s', s' ⊆ s ∧ s'.card ≤ d ∧ s ⊆ mulSpan s' := by
classical
obtain ⟨s', hs'⟩ :=
(s.powerset.filter fun s' : Finset α ↦ MulDissociated (s' : Set α)).exists_maximal
⟨∅, mem_filter.2 ⟨empty_mem_powerset _, by simp⟩⟩
simp only [mem_filter, mem_powerset] at hs'
refine ⟨s', hs'.1.1, hs _ hs'.1.1 hs'.1.2, fun a ha ↦ ?_⟩
by_cases ha' : a ∈ s'
· exact subset_mulSpan ha'
obtain ⟨t, u, ht, hu, htu⟩ :=
not_mulDissociated_iff_exists_disjoint.1 fun h ↦
hs'.not_gt ⟨insert_subset_iff.2 ⟨ha, hs'.1.1⟩, h⟩ <| ssubset_insert ha'
by_cases hat : a ∈ t
· have : a = (∏ b ∈ u, b) / ∏ b ∈ t.erase a, b := by rw [prod_erase_eq_div hat, htu.2.2, div_div_self']
rw [this]
exact
prod_div_prod_mem_mulSpan ((subset_insert_iff_of_notMem <| disjoint_left.1 htu.1 hat).1 hu)
(subset_insert_iff.1 ht)
rw [coe_subset, subset_insert_iff_of_notMem hat] at ht
by_cases hau : a ∈ u
· have : a = (∏ b ∈ t, b) / ∏ b ∈ u.erase a, b := by rw [prod_erase_eq_div hau, htu.2.2, div_div_self']
rw [this]
exact prod_div_prod_mem_mulSpan ht (subset_insert_iff.1 hu)
· rw [coe_subset, subset_insert_iff_of_notMem hau] at hu
cases not_mulDissociated_iff_exists_disjoint.2 ⟨t, u, ht, hu, htu⟩ hs'.1.2
