copyBase — Mathlib

English

Create a copy of M with a base predicate and ground set defeq to M.

Русский

Создать копию матроида M с предикатом базы и тем же основанием E.

LaTeX

$$copyBase(M, E, IsBase, hE, h) defines a matroid with IsBase as bases predicate$$

Lean4

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

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