empty_isBase_iff — Mathlib

English

For any matroid M, M.IsBase ∅ if and only if M = loopyOn M.E.

Русский

Для любого матроидa M, M.IsBase ∅ тогда и только тогда, когда M = loopyOn(M.E).

LaTeX

$$$ M.IsBase \\emptyset \\iff M = \\mathrm{loopyOn}(M.E) $$$

Lean4

theorem empty_isBase_iff : M.IsBase ∅ ↔ M = loopyOn M.E :=
  by
  simp only [isBase_iff_maximal_indep, Maximal, empty_indep, le_eq_subset, empty_subset, subset_empty_iff, true_implies,
    true_and, ext_iff_indep, loopyOn_ground, loopyOn_indep_iff]
  exact ⟨fun h I _ ↦ ⟨@h _, fun hI ↦ by simp [hI]⟩, fun h I hI ↦ (h hI.subset_ground).1 hI⟩

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