contract_isNonloop_iff — Mathlib

English

An element e is nonloop in the contracted matroid M / C if and only if e belongs to the ground set E but not to the closure of C.

Русский

Элемент e является не петлей в M / C тогда и только тогда, когда он принадлежит множеству E и не принадлежит замыканию C.

LaTeX

$$$(M / C).IsNonloop e \\iff e \\in M.E \\setminus M.closure C$$

Lean4

@[simp]
theorem contract_isNonloop_iff : (M ／ C).IsNonloop e ↔ e ∈ M.E \ M.closure C :=
  by
  rw [isNonloop_iff_mem_compl_loops, contract_ground, contract_loops_eq]
  refine ⟨fun ⟨he, heC⟩ ↦ ⟨he.1, fun h ↦ heC ⟨h, he.2⟩⟩, fun h ↦ ⟨⟨h.1, fun heC ↦ h.2 ?_⟩, fun h' ↦ h.2 h'.1⟩⟩
  rw [← closure_inter_ground]
  exact (M.subset_closure (C ∩ M.E)) ⟨heC, h.1⟩

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