English
If hB is a base, I ⊂ B, and hB' is a base, then there exists e ∈ B' \\ I such that I ∪ {e} is independent.
Русский
Если B — база, I ⊂ B, и B' — база, существует e ∈ B' \\ I такое, что I ∪ {e} независимо.
LaTeX
$$M.IsBase(B) → I ⊂ B → M.IsBase(B') → ∃ e ∈ B' \\ I, M.Indep(I ∪ {e})$$
Lean4
/-- create a copy of `M : Matroid α` with independence and base predicates and ground set defeq
to supplied arguments that are provably equal to those of `M`. -/
@[simps]
def copy (M : Matroid α) (E : Set α) (IsBase Indep : Set α → Prop) (hE : E = M.E) (hB : ∀ B, IsBase B ↔ M.IsBase B)
(hI : ∀ I, Indep I ↔ M.Indep I) : Matroid α where
E := E
IsBase := IsBase
Indep := Indep
indep_iff' _ := by simp_rw [hI, hB, M.indep_iff]
exists_isBase := by
simp_rw [hB]
exact M.exists_isBase
isBase_exchange := by
simp_rw [show IsBase = M.IsBase from funext (by simp [hB])]
exact M.isBase_exchange
maximality := by
simp_rw [hE, show Indep = M.Indep from funext (by simp [hI])]
exact M.maximality
subset_ground := by
simp_rw [hE, hB]
exact M.subset_ground
