uniqueBaseOn_restrict' — Mathlib

English

Restriction of the matroid (uniqueBaseOn I E) to R equals the matroid uniqueBaseOn (I ∩ R ∩ E) R.

Русский

Ограничение матроида (uniqueBaseOn I E) до R равно матроиду uniqueBaseOn (I ∩ R ∩ E) R.

LaTeX

$$$(\mathrm{uniqueBaseOn}(I,E))|_R = \mathrm{uniqueBaseOn}(I \cap R \cap E) R$$$

Lean4

theorem uniqueBaseOn_restrict' (I E R : Set α) : (uniqueBaseOn I E) ↾ R = uniqueBaseOn (I ∩ R ∩ E) R :=
  by
  simp_rw [ext_iff_indep, restrict_ground_eq, uniqueBaseOn_ground, true_and, restrict_indep_iff,
    uniqueBaseOn_indep_iff', subset_inter_iff]
  tauto

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