closure_diff_singleton_eq_closure

English

Let M be a matroid on α and X ⊆ α, e ∈ α. If e ∈ closure_M(X \ {e}), then closure_M(X \ {e}) = closure_M(X).

Русский

Пусть M — матроид на α и X ⊆ α, e ∈ α. Если e принадлежит замыканию M над X \ {e}, то замыкание X \ {e} равно замыканию X.

LaTeX

$$$$ e \in \operatorname{cl}_M(X \setminus \{e\}) \Rightarrow \operatorname{cl}_M(X \setminus \{e\}) = \operatorname{cl}_M(X). $$$$

Lean4

theorem closure_diff_singleton_eq_closure (h : e ∈ M.closure (X \ { e })) : M.closure (X \ { e }) = M.closure X :=
  closure_diff_eq_self (by simpa)

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