mem_closure_diff_singleton_of_mem

English

If e ∈ C and C is a circuit, then e lies in the closure of C \\ {e}.

Русский

Если e ∈ C и C является окружностью, тогда e лежит в замыкании C \\ {e}.

LaTeX

$$$\\forall {\\alpha} {M : Matroid \\alpha} {C} (hC : M.IsCircuit C) (e : \\alpha), e ∈ C \\to e \\in M.closure (C \\ { e })$$$

Lean4

theorem mem_closure_diff_singleton_of_mem (hC : M.IsCircuit C) (heC : e ∈ C) : e ∈ M.closure (C \ { e }) :=
  hC.subset_closure_diff_singleton e heC

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