closure_diff_singleton_eq — Mathlib

English

For any circuit C, closure of C after removing an element e equals closure of C.

Русский

Для любой окружности C замыкание после удаления элемента e равно замыканию C.

LaTeX

$$$\\forall {\\alpha} {M : Matroid \\alpha} {C : Set \\alpha}, M.IsCircuit C \\to ∀ e, M.closure (C \\ {e}) = M.closure C$$$

Lean4

theorem closure_diff_singleton_eq (hC : M.IsCircuit C) (e : α) : M.closure (C \ { e }) = M.closure C :=
  (em (e ∈ C)).elim (fun he ↦ by rw [(hC.diff_singleton_isBasis he).closure_eq_closure])
    (fun he ↦ by rw [diff_singleton_eq_self he])

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