restrict_spanning_iff' — Mathlib

English

For a matroid M and subsets R,S, the restriction M|R spans S if and only if R ∩ E ⊆ closure(S) and S ⊆ R.

Русский

Для матроида M и подмножеств R,S ограничение M|R охватывает S тогда и только тогда, когда R ∩ E ⊆ замыкание(S) и S ⊆ R.

LaTeX

$$$ (M \\restriction R).Spanning S \\iff (R \\cap M.E) \\subseteq M.closure S \\land S \\subseteq R $$$

Lean4

theorem restrict_spanning_iff' : (M ↾ R).Spanning S ↔ R ∩ M.E ⊆ M.closure S ∧ S ⊆ R :=
  by
  rw [spanning_iff, restrict_closure_eq', restrict_ground_eq, and_congr_left_iff, diff_eq_compl_inter, ←
    union_inter_distrib_right, inter_eq_right, union_comm, ← diff_subset_iff, diff_compl]
  intro hSR
  rw [inter_eq_self_of_subset_left hSR]

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