English
For a structure IndepMatroid, the matroid-level independence coincides with the given independence predicate.
Русский
У структуры IndepMatroid независимость на уровне матроида совпадает с заданной независимостью.
LaTeX
$$$ \forall {I}: M.matroid.Indep I \iff M.Indep I $$$
Lean4
/-- An `M : IndepMatroid α` gives a `Matroid α` whose bases are the maximal `M`-independent sets. -/
@[simps]
protected def matroid (M : IndepMatroid α) : Matroid α
where
E := M.E
IsBase := Maximal M.Indep
Indep := M.Indep
indep_iff' := by
refine fun I ↦ ⟨fun h ↦ ?_, fun ⟨B, ⟨h, _⟩, hIB'⟩ ↦ M.indep_subset h hIB'⟩
obtain ⟨J, hIJ, hmax⟩ := M.indep_maximal M.E rfl.subset I h (M.subset_ground I h)
rw [maximal_and_iff_right_of_imp M.subset_ground] at hmax
exact ⟨J, hmax.1, hIJ⟩
exists_isBase :=
by
obtain ⟨B, -, hB⟩ := M.indep_maximal M.E rfl.subset ∅ M.indep_empty <| empty_subset _
rw [maximal_and_iff_right_of_imp M.subset_ground] at hB
exact ⟨B, hB.1⟩
isBase_exchange B B' hB hB' e
he :=
by
have hnotmax : ¬Maximal M.Indep (B \ { e }) := fun h ↦
h.not_prop_of_ssuperset (diff_singleton_ssubset.2 he.1) hB.prop
obtain ⟨f, hf, hfB⟩ := M.indep_aug (M.indep_subset hB.prop diff_subset) hnotmax hB'
replace hf := show f ∈ B' \ B by simpa [show f ≠ e by rintro rfl; exact he.2 hf.1] using hf
refine ⟨f, hf, by_contra fun hnot ↦ ?_⟩
obtain ⟨x, hxB, hind⟩ := M.indep_aug hfB hnot hB
obtain ⟨-, rfl⟩ : _ ∧ x = e := by simpa [hxB.1] using hxB
refine hB.not_prop_of_ssuperset ?_ hind
rw [insert_comm, insert_diff_singleton, insert_eq_of_mem he.1]
exact ssubset_insert hf.2
maximality := M.indep_maximal
subset_ground B hB := M.subset_ground B hB.1
