copyIndep — Mathlib

English

Create a copy of M with the same ground set and an independence predicate that is equivalent to M.Indep.

Русский

Создать копию матроида M с тем же ground set и предикатом независимости, равным M.Indep.

LaTeX

$$copyIndep(M, E, Indep, hE, h) defines a matroid with E as ground set and Indep ≡ M.Indep$$

Lean4

/-- create a copy of `M : Matroid α` with an independence predicate and ground set defeq
to supplied arguments that are provably equal to those of `M`. -/
@[simps!]
def copyIndep (M : Matroid α) (E : Set α) (Indep : Set α → Prop) (hE : E = M.E) (h : ∀ I, Indep I ↔ M.Indep I) :
    Matroid α :=
  M.copy E M.IsBase Indep hE (fun _ ↦ Iff.rfl) h

Похожие утверждения