English
If there exists a matroid M on α whose ground is E and whose independence predicate agrees with a given Indep, then one can form a Matroid on α from this data.
Русский
Если существует матроид M на α с опорным множеством E и независимость совпадает с данным Indep, то из этих данных можно построить матроид на α.
LaTeX
$$$\\exists M : Matroid\\ α, E = M.E \\land \\forall I, M.Indep I \\iff Indep I$$$
Lean4
/-- Construct an `Matroid` from an independence predicate that agrees with that of some matroid `M`.
This is computable even if `M` is only known existentially, or when `M` exists for different
reasons in different cases. This can also be used to change the independence predicate to a
more useful definitional form. -/
@[simps! E]
protected def ofExistsMatroid (E : Set α) (Indep : Set α → Prop)
(hM : ∃ (M : Matroid α), E = M.E ∧ ∀ I, M.Indep I ↔ Indep I) : Matroid α :=
IndepMatroid.matroid <|
have hex : ∃ (M : Matroid α), E = M.E ∧ M.Indep = Indep := by obtain ⟨M, rfl, h⟩ := hM;
refine ⟨_, rfl, funext (by simp [h])⟩
IndepMatroid.mk (E := E) (Indep := Indep) (indep_empty := by obtain ⟨M, -, rfl⟩ := hex; exact M.empty_indep)
(indep_subset := by obtain ⟨M, -, rfl⟩ := hex; exact fun I J hJ hIJ ↦ hJ.subset hIJ) (indep_aug := by
obtain ⟨M, -, rfl⟩ := hex; exact Indep.exists_insert_of_not_maximal M) (indep_maximal := by
obtain ⟨M, rfl, rfl⟩ := hex; exact M.existsMaximalSubsetProperty_indep) (subset_ground := by
obtain ⟨M, rfl, rfl⟩ := hex; exact fun I ↦ Indep.subset_ground)
