restrict_eq_freeOn_iff — Mathlib

English

For any M and I, the restriction M|I equals freeOn I if and only if I is independent in M.

Русский

Для любого матроида M и множества I: ограничение M по I равно freeOn(I) тогда и только тогда, когда I независимо в M.

LaTeX

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

Lean4

theorem restrict_eq_freeOn_iff : M ↾ I = freeOn I ↔ M.Indep I := by
  rw [eq_freeOn_iff, and_iff_right M.restrict_ground_eq, restrict_indep_iff, and_iff_left Subset.rfl]

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