English
If E is finite and Indep satisfies the independence axioms with augmentation and ground-subset conditions, then the construction of IndepMatroid ofFinite yields a well-defined independence structure on α.
Русский
Если E конечна и Indep удовлетворяет аксиомам независимости с дополнением и условиям подмножества к опорному множеству, то конструктор IndepMatroid.ofFinite задаёт корректную структуру независимости на α.
LaTeX
$$$\\mathrm{IndepMatroid.ofFinite}\\,(hE:E.Finite)\\, Indep\\, indep\\_empty\\, indep\\_subset\\, indep\\_aug\\, subset\\_ground :\\ IndepMatroid\\ α$$$
Lean4
/-- If `E` is finite, then any collection of subsets of `E` satisfying
the usual independence axioms determines a matroid -/
protected def ofFinite {E : Set α} (hE : E.Finite) (Indep : Set α → Prop) (indep_empty : Indep ∅)
(indep_subset : ∀ ⦃I J⦄, Indep J → I ⊆ J → Indep I)
(indep_aug : ∀ ⦃I J⦄, Indep I → Indep J → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
(subset_ground : ∀ ⦃I⦄, Indep I → I ⊆ E) : IndepMatroid α :=
IndepMatroid.ofBddAugment (E := E) (Indep := Indep) (indep_empty := indep_empty) (indep_subset := indep_subset)
(indep_aug := by
refine fun {I J} hI hJ hIJ ↦ indep_aug hI hJ ?_
rwa [← Nat.cast_lt (α := ℕ∞), (hE.subset (subset_ground hJ)).cast_ncard_eq,
(hE.subset (subset_ground hI)).cast_ncard_eq])
(indep_bdd :=
⟨E.ncard, fun I hI ↦ by
rw [hE.cast_ncard_eq]
exact encard_le_encard <| subset_ground hI⟩)
(subset_ground := subset_ground)
