closure_subset_closure_of_subset_closure

English

Let M be a matroid on α. If X is contained in the closure of Y, then the closure of X is contained in the closure of Y.

Русский

Пусть M — матроид на α. Если X ⊆ cl(Y), то cl(X) ⊆ cl(Y).

LaTeX

$$$X \\subseteq \\operatorname{cl}(Y) \\Rightarrow \\operatorname{cl}(X) \\subseteq \\operatorname{cl}(Y)$$$

Lean4

theorem closure_subset_closure_of_subset_closure (hXY : X ⊆ M.closure Y) : M.closure X ⊆ M.closure Y :=
  (M.closure_subset_closure hXY).trans_eq (M.closure_closure Y)

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