eq_of_restrictSubtype_eq — Mathlib

English

If M.E = E and N.E = E and M.restrictSubtype E = N.restrictSubtype E, then M = N.

Русский

Если M.Е = E и N.Е = E и M.restrictSubtype E = N.restrictSubtype E, то M = N.

LaTeX

$$Eq M.E E → Eq N.E E → Eq (M.restrictSubtype E) (N.restrictSubtype E) → Eq M N$$

Lean4

theorem eq_of_restrictSubtype_eq {N : Matroid α} (hM : M.E = E) (hN : N.E = E)
    (h : M.restrictSubtype E = N.restrictSubtype E) : M = N :=
  by
  subst hM
  refine ext_indep (by rw [hN]) (fun I hI ↦ ?_)
  rwa [← restrictSubtype_indep_iff_of_subset hI, h, restrictSubtype_indep_iff_of_subset]

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