setOf_indep_eq — Mathlib

English

Let M be a matroid on α. A subset I of α is independent exactly when I is contained in some base of M.

Русский

Пусть M — матроид на α. Подмножество I ⊆ α является независимым тогда и только тогда, когда оно содержится в некоторой базе M.

LaTeX

$$$\{ I \subseteq \alpha \mid M.Indep I \} = \{ I \subseteq \alpha \mid \exists B\,(M.IsBase B \land I \subseteq B) \}$$$

Lean4

theorem setOf_indep_eq (M : Matroid α) : {I | M.Indep I} = lowerClosure ({B | M.IsBase B}) := by
  simp_rw [indep_iff, lowerClosure, LowerSet.coe_mk, mem_setOf, le_eq_subset]

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