English
Given a ground set E and an independence predicate Indep satisfying the standard axioms (empty, hereditary, augmentation, and compactness on finite subsets, and subset-ground), there is an IndepMatroid structure on E with Indep as its independence predicate.
Русский
При данных грунтовых множествах E и предикате независимости Indep, удовлетворяющих стандартным аксиомам (пустое, наследование, дополнение и компактность на конечных подмножествах, а также подмножество грунта), существует структура IndepMatroid на E с независимостью Indep.
LaTeX
$$$ \text{IndepMatroid.ofFinitary}(E, Indep, \dots) \text{ существует и задаёт } Indep \text{ на } E$$$
Lean4
/-- If `Indep` has the 'compactness' property that each set `I` satisfies `Indep I` if and only if
`Indep J` for every finite subset `J` of `I`,
then an `IndepMatroid` can be constructed without proving the maximality axiom.
This needs choice, since it can be used to prove that every vector space has a basis. -/
@[simps E]
protected def ofFinitary (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅)
(indep_subset : ∀ ⦃I J⦄, Indep J → I ⊆ J → Indep I)
(indep_aug : ∀ ⦃I B⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I))
(indep_compact : ∀ I, (∀ J, J ⊆ I → J.Finite → Indep J) → Indep I) (subset_ground : ∀ I, Indep I → I ⊆ E) :
IndepMatroid α where
E := E
Indep := Indep
indep_empty := indep_empty
indep_subset := indep_subset
indep_aug := indep_aug
indep_maximal := by
refine fun X _ I hI hIX ↦ zorn_subset_nonempty {Y | Indep Y ∧ Y ⊆ X} ?_ I ⟨hI, hIX⟩
refine fun Is hIs hchain _ ↦ ⟨⋃₀ Is, ⟨?_, sUnion_subset fun Y hY ↦ (hIs hY).2⟩, fun _ ↦ subset_sUnion_of_mem⟩
refine indep_compact _ fun J hJ hJfin ↦ ?_
have hchoose : ∀ e, e ∈ J → ∃ I, I ∈ Is ∧ (e : α) ∈ I := fun _ he ↦ mem_sUnion.1 <| hJ he
choose! f hf using hchoose
refine J.eq_empty_or_nonempty.elim (fun hJ ↦ hJ ▸ indep_empty) (fun hne ↦ ?_)
obtain ⟨x, hxJ, hxmax⟩ := Finite.exists_maximalFor f _ hJfin hne
refine indep_subset (hIs (hf x hxJ).1).1 fun y hyJ ↦ ?_
obtain (hle | hle) := hchain.total (hf _ hxJ).1 (hf _ hyJ).1
· exact hxmax hyJ hle <| (hf _ hyJ).2
· exact hle (hf _ hyJ).2
subset_ground := subset_ground
