matroid_closure_of_subsingleton — Mathlib

English

If A is a subsingleton, then the matroid closure of any subset s equals s itself.

Русский

Если A — пододиночно, то замыкание матроида множества s равно самому s.

LaTeX

$$$ [Subsingleton\\; A] \\Rightarrow (\\mathrm{matroid} \\; R\\, A).closure(s) = s $$$

Lean4

theorem matroid_closure_of_subsingleton [Subsingleton A] (s : Set A) : (matroid R A).closure s = s :=
  by
  simp_rw [Matroid.closure, matroid_isFlat_of_subsingleton, true_and, matroid_e, inter_univ]
  exact subset_antisymm (sInter_subset_of_mem <| subset_refl s) (subset_sInter fun _ ↦ id)

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