contract_isLoop_iff_mem_closure — Mathlib

English

An element e is a loop in M / C if and only if e lies in the closure of C and e is not in C.

Русский

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

LaTeX

$$$(M / C).IsLoop e \\iff (e \\in M.closure C) \\land e \\notin C$$$

Lean4

@[simp]
theorem contract_isLoop_iff_mem_closure : (M ／ C).IsLoop e ↔ e ∈ M.closure C ∧ e ∉ C :=
  by
  obtain ⟨I, hI⟩ := M.exists_isBasis' C
  rw [hI.contract_eq_contract_delete, delete_isLoop_iff, ← singleton_dep, hI.indep.contract_dep_iff, singleton_union,
    hI.indep.insert_dep_iff, hI.closure_eq_closure]
  by_cases heI : e ∈ I
  · simp [heI, hI.subset heI]
  simp [heI, and_comm]

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