uniqueBaseOn_isBasis_iff — Mathlib

English

M restricted to I equals freeOn I if and only if I is independent in M.

Русский

Матроидa M ограничение к I равно freeOn I тогда, когда I независимо в M.

LaTeX

$$$ M \restriction I = freeOn I \iff M.Indep I $$$

Lean4

theorem uniqueBaseOn_isBasis_iff (hX : X ⊆ E) : (uniqueBaseOn I E).IsBasis J X ↔ J = X ∩ I :=
  by
  rw [isBasis_iff_maximal]
  exact maximal_iff_eq (by simp [inter_subset_left.trans hX]) (by simp +contextual)

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