English
An independence predicate on Finset α that satisfies finite matroid axioms determines a finitary matroid on α.
Русский
Аксиомы конечного матроида для предиката независимости на конечных множествах определяют конечный матроид на α.
LaTeX
$$$\\mathrm{IndepMatroid.ofFinset}\\ (E)\\; Indep\\; indep\\_empty\\; indep\\_subset\\; indep\\_aug\\; subset\\_ground : \\ IndepMatroid \\ α$$$
Lean4
/-- An independence predicate on `Finset α` that obeys the finite matroid axioms determines a
finitary matroid on `α`. -/
protected def ofFinset [DecidableEq α] (E : Set α) (Indep : Finset α → Prop) (indep_empty : Indep ∅)
(indep_subset : ∀ ⦃I J⦄, Indep J → I ⊆ J → Indep I)
(indep_aug : ∀ ⦃I J⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
(subset_ground : ∀ ⦃I⦄, Indep I → (I : Set α) ⊆ E) : IndepMatroid α :=
IndepMatroid.ofFinitaryCardAugment (E := E) (Indep := (fun I ↦ (∀ (J : Finset α), (J : Set α) ⊆ I → Indep J)))
(indep_empty := by simpa [subset_empty_iff]) (indep_subset := (fun _ _ hJ hIJ _ hKI ↦ hJ _ (hKI.trans hIJ)))
(indep_aug := by
intro I J hI hIfin hJ hJfin hIJ
rw [ncard_eq_toFinset_card _ hIfin, ncard_eq_toFinset_card _ hJfin] at hIJ
have aug := indep_aug (hI _ (by simp)) (hJ _ (by simp)) hIJ
simp only [Finite.mem_toFinset] at aug
obtain ⟨e, heJ, heI, hi⟩ := aug
exact ⟨e, heJ, heI, fun K hK ↦ indep_subset hi <| Finset.coe_subset.1 (by simpa)⟩) (indep_compact := fun _ h J hJ ↦
h _ hJ J.finite_toSet _ Subset.rfl) (subset_ground := fun I hI x hxI ↦ by
simpa using subset_ground <| hI { x } (by simpa))
