contract_loops_eq — Mathlib

English

The set of loops after contracting by C equals the loop set of M restricted to the complement of C.

Русский

Множество петель после сокращения по C равно множеству петель матроида M над комплементом C.

LaTeX

$$$(M / C).loops = M.loops \\ C$$

Lean4

@[simp]
theorem contract_loops_eq (M : Matroid α) (C : Set α) : (M ／ C).loops = M.closure C \ C := by
  simp [Set.ext_iff, ← isLoop_iff, contract_isLoop_iff_mem_closure]

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