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⟩⟩