matroid_isFlat_of_subsingleton — Mathlib

English

If A is a subsingleton, then every subset s of A is flat in the matroid over R.

Русский

Если A — пододиночно, то любое подмножество s ⊆ A является плоскостью в матроиде над R.

LaTeX

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

Lean4

theorem matroid_isFlat_of_subsingleton [Subsingleton A] (s : Set A) : (matroid R A).IsFlat s :=
  by
  simp_rw [Matroid.isFlat_iff, matroid_e, subset_univ, and_true, matroid_isBasis_iff_of_subsingleton]
  exact fun I X hIs hIX ↦ (hIX.symm.trans hIs).subset

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