IsBasis — Mathlib

English

A Basis for a set X ⊆ E is a maximal independent subset of X, with X ⊆ E.

Русский

База для множества X ⊆ E — максимальное независимое подмножество X, причём X ⊆ E.

LaTeX

$$IsBasis(M, I, X) := Maximal (λ A, M.Indep A ∧ A ⊆ X) I ∧ X ⊆ E$$

Lean4

/-- A Basis for a set `X ⊆ M.E` is a maximal independent subset of `X`
  (Often in the literature, the word 'Basis' is used to refer to what we call a 'Base'). -/
def IsBasis (M : Matroid α) (I X : Set α) : Prop :=
  Maximal (fun A ↦ M.Indep A ∧ A ⊆ X) I ∧ X ⊆ M.E

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