closure_empty_eq_ground_iff — Mathlib

English

For any matroid M with ground E, closure of the empty set equals E if and only if M equals loopyOn(E).

Русский

Для матроида M с основанием E замыкание пустого множества равно E тогда и только тогда, когда M равно loopyOn(E).

LaTeX

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

Lean4

theorem closure_empty_eq_ground_iff : M.closure ∅ = M.E ↔ M = loopyOn M.E :=
  by
  refine ⟨fun h ↦ ext_closure ?_, fun h ↦ by rw [h, loopyOn_closure_eq, loopyOn_ground]⟩
  refine fun X ↦ subset_antisymm (by simp [closure_subset_ground]) ?_
  rw [loopyOn_closure_eq, ← h]
  exact M.closure_mono (empty_subset _)

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