English
In the finitary setting, independence on Finset α agrees with the constructed independence predicate on Finset elements.
Русский
В конечной настройке независимость на Finset α совпадает с построенным предикатом независимости на конечных множествах.
LaTeX
$$$(\\mathrm{ofFinset}\\; E\\; Indep\\; indep\\_empty\\; indep\\_subset\\; indep\\_aug\\; subset\\_ground).Indep I \\iff Indep I$$$
Lean4
@[simp]
theorem ofFinset_indep [DecidableEq α] (E : Set α) Indep indep_empty indep_subset indep_aug subset_ground
{I : Finset α} :
(IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).Indep I ↔ Indep I :=
by
simp only [IndepMatroid.ofFinset, ofFinitaryCardAugment_indep, Finset.coe_subset]
exact ⟨fun h ↦ h _ Subset.rfl, fun h J hJI ↦ indep_subset h hJI⟩
