freeOn_closure_eq — Mathlib

English

Let E and X be subsets of the ground set. In the matroid obtained by freely adjoining E, the closure of X is exactly X ∩ E.

Русский

Пусть E и X — подмножества множества. Замыкание X в матроиде, полученном свободно присоединяя E, равно X ∩ E.

LaTeX

$$$\\mathrm{cl}_{\\mathrm{freeOn}(E)}(X) = X \\cap E$$$

Lean4

@[simp]
theorem freeOn_closure_eq (E X : Set α) : (freeOn E).closure X = X ∩ E := by
  simp +contextual [← closure_inter_ground _ X, Set.ext_iff, and_comm, insert_subset_iff, freeOn_indep_iff,
    (freeOn_indep inter_subset_right).mem_closure_iff']

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