eq_loopyOn_iff — Mathlib

English

A matroid M equals loopyOn E if and only if M.E = E and every X ⊆ M.E with M.Indep X implies X = ∅.

Русский

Матроид M равен loopyOn E тогда и только тогда, когда M.E = E и для всех X ⊆ M.E, если M.Indep X, то X = ∅.

LaTeX

$$$ M = \\mathrm{loopyOn}(E) \\iff (M.E = E) \\land (\\forall X \\subseteq M.E, M.Indep X \\rightarrow X = \\emptyset)$$$

Lean4

theorem eq_loopyOn_iff : M = loopyOn E ↔ M.E = E ∧ ∀ X ⊆ M.E, M.Indep X → X = ∅ :=
  by
  simp only [ext_iff_indep, loopyOn_ground, loopyOn_indep_iff, and_congr_right_iff]
  rintro rfl
  refine ⟨fun h I hI ↦ (h hI).1, fun h I hIE ↦ ⟨h I hIE, by rintro rfl; simp⟩⟩

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