English
A strengthened form of the Finset-based independence yields an equivalence between Indep(I) and all finite subfinset independences contained in I.
Русский
Усиленная форма независимости на Finset даёт эквивалентность Indep(I) и всех независимостей подмножества I.
LaTeX
$$$\\mathrm{ofFinset\\_indep'}\\; Indep\\; indep\\_empty\\; indep\\_subset\\; indep\\_aug\\; subset\\_ground\\; \\{I\\}$$$
Lean4
/-- This can't be `@[simp]`, because it would cause the more useful
`Matroid.ofIndepFinset_apply` not to be in simp normal form. -/
theorem ofFinset_indep' [DecidableEq α] (E : Set α) Indep indep_empty indep_subset indep_aug subset_ground {I : Set α} :
(IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).Indep I ↔
∀ (J : Finset α), (J : Set α) ⊆ I → Indep J :=
by simp only [IndepMatroid.ofFinset, ofFinitaryCardAugment_indep]
