uniqueBaseOn_closure_eq — Mathlib

English

In the matroid uniqueBaseOn I E, the closure of X is (X ∩ I ∩ E) ∪ (E \\ I).

Русский

В матроиде uniqueBaseOn I E замыкание X равно (X ∩ I ∩ E) ∪ (E \ I).

LaTeX

$$$\\mathrm{cl}_{\\mathrm{uniqueBaseOn}(I,E)}(X) = (X \\cap I \\cap E) \\cup (E \\setminus I)$$$

Lean4

@[simp]
theorem uniqueBaseOn_closure_eq (I E X : Set α) : (uniqueBaseOn I E).closure X = (X ∩ I ∩ E) ∪ (E \ I) := by
  rw [uniqueBaseOn, restrict_closure_eq', freeOn_closure_eq, inter_right_comm, inter_assoc (c := E), inter_self,
    inter_right_comm, freeOn_ground]

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