English
A coloop e is equivalent to a universal closure condition: the mapping with closure and membership coincides for all X ⊆ E.
Русский
Колооп e эквивалентен универсальному условию по замыканию: свойство замыкания и принадлежности верны для всех X ⊆ E.
LaTeX
$$$M.IsColoop e \\iff (\\forall X \\ (X \\subseteq M.E \\to (e \\in M.closure X \\iff e \\in X)))$$$
Lean4
/-- A version of `Matroid.isColoop_iff_forall_mem_closure_iff_mem` where we only quantify
over subsets of the ground set. -/
theorem isColoop_iff_forall_mem_closure_iff_mem' :
M.IsColoop e ↔ (∀ X, X ⊆ M.E → (e ∈ M.closure X ↔ e ∈ X)) ∧ e ∈ M.E :=
by
refine
⟨fun h ↦ ⟨fun X _ ↦ isColoop_iff_forall_mem_closure_iff_mem.1 h X, h.mem_ground⟩, fun ⟨h, he⟩ ↦
isColoop_iff_forall_mem_closure_iff_mem.2 fun X ↦ ?_⟩
rw [← closure_inter_ground, h _ inter_subset_right, mem_inter_iff, and_iff_left he]
