English
If there is a bound on encard, then an augmentation axiom holds for IndepMatroid built from Bdd structure.
Русский
Если существует ограничение на encard, то выполняется аксиома augment для IndepMatroid, построенного из структуры Bdd.
LaTeX
$$IndepMatroid.ofBddAugment E Indep indep_empty indep_subset indep_aug indep_bdd subset_ground$$
Lean4
/-- If there is an absolute upper bound on the size of an independent set, then matroids
can be defined using an 'augmentation' axiom similar to the standard definition of
finite matroids for independent sets. -/
protected def ofBddAugment (E : Set α) (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.encard < J.encard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
(indep_bdd : ∃ (n : ℕ), ∀ I, Indep I → I.encard ≤ n) (subset_ground : ∀ I, Indep I → I ⊆ E) : IndepMatroid α :=
IndepMatroid.ofBdd (E := E) (Indep := Indep) (indep_empty := indep_empty) (indep_subset := indep_subset) (indep_aug :=
by
rintro I B hI hImax hBmax
suffices hcard : I.encard < B.encard
by
obtain ⟨e, heB, heI, hi⟩ := indep_aug hI hBmax.prop hcard
exact ⟨e, ⟨heB, heI⟩, hi⟩
refine lt_of_not_ge fun hle ↦ ?_
obtain ⟨x, hxnot, hxI⟩ := exists_insert_of_not_maximal indep_subset hI hImax
have hlt : B.encard < (insert x I).encard :=
by
rwa [encard_insert_of_notMem hxnot, ← not_le, ENat.add_one_le_iff, not_lt]
rw [encard_ne_top_iff]
obtain ⟨n, hn⟩ := indep_bdd
exact finite_of_encard_le_coe (hn _ hI)
obtain ⟨y, -, hyB, hi⟩ := indep_aug hBmax.prop hxI hlt
exact hBmax.not_prop_of_ssuperset (ssubset_insert hyB) hi) (indep_bdd := indep_bdd) (subset_ground := subset_ground)
