uniqueBaseOn_dual_eq — Mathlib

English

The dual of the matroid uniqueBaseOn I E equals the matroid uniqueBaseOn (E \ I) E.

Русский

Дуальная матроидa from uniqueBaseOn I E равна матрoиду uniqueBaseOn (E \ I) E.

LaTeX

$$$(\mathrm{uniqueBaseOn}(I,E))^{\star} = \mathrm{uniqueBaseOn}(E \setminus I, E)$$$

Lean4

@[simp]
theorem uniqueBaseOn_dual_eq (I E : Set α) : (uniqueBaseOn I E)✶ = uniqueBaseOn (E \ I) E :=
  by
  rw [← uniqueBaseOn_inter_ground_eq]
  refine ext_isBase rfl (fun B (hB : B ⊆ E) ↦ ?_)
  rw [dual_isBase_iff, uniqueBaseOn_isBase_iff inter_subset_right, uniqueBaseOn_isBase_iff diff_subset,
    uniqueBaseOn_ground]
  exact ⟨fun h ↦ by rw [← diff_diff_cancel_left hB, h, diff_inter_self_eq_diff], fun h ↦ by rw [h, inter_comm I]; simp⟩

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