existsMaximalSubsetProperty_indep

English

For any X ⊆ E, there exists a maximal subset of X with respect to independence.

Русский

Для любого X ⊆ E существует максимальное по включению подмножество с независимостью.

LaTeX

$$∃ S ⊆ X, M.Indep S ∧ ∀ T ⊆ X, M.Indep T ∧ S ⊆ T → T = S$$

Lean4

/-- Matroids obey the maximality axiom -/
theorem existsMaximalSubsetProperty_indep (M : Matroid α) : ∀ X, X ⊆ M.E → ExistsMaximalSubsetProperty M.Indep X :=
  M.maximality

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