restrictSubtype_dual — Mathlib

English

Let M be a matroid on a ground set α and E be a subset of α. The dual of the restriction of M to E is the same as the restriction to E of the dual matroid, i.e. (M|E)^* = M^*|E.

Русский

Пусть M — матроид на множества α и E ⊆ α. Двойственный ограничение M к E равно ограничению двойственного матroid к E: (M|E)^* = M^*|E.

LaTeX

$$$ (M|_E)^* = M^*|_E $$$

Lean4

@[simp]
theorem restrictSubtype_dual : (M.restrictSubtype M.E)✶ = M✶.restrictSubtype M.E :=
  by
  rw [restrictSubtype, ← comapOn_preimage_eq, comapOn_dual_eq_of_bijOn, restrict_ground_eq_self, ← dual_ground,
    comapOn_preimage_eq, restrictSubtype, restrict_ground_eq_self]
  exact ⟨by simp [MapsTo], Subtype.val_injective.injOn, by simp [SurjOn]⟩

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