restrictSubtype_inter_indep_iff — Mathlib

English

Independence in the restricted matroid on X for X ∩ I corresponds to independence in M.

Русский

Независимость в ограничении на X для X ∩ I соответствует независимости в M.

LaTeX

$$$(M.restrictSubtype X).Indep (X ∩ I) \iff M.Indep (X ∩ I)$$$

Lean4

theorem restrictSubtype_inter_indep_iff : (M.restrictSubtype X).Indep (X ↓∩ I) ↔ M.Indep (X ∩ I) := by
  simp [restrictSubtype, Subtype.val_injective.injOn]

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