closure — Mathlib

English

Let M be a matroid on α. If a subset X has finite rank in M, then its closure has finite rank in M.

Русский

Пусть M — матроид на α. Если подмножество X имеет конечный ранг в M, то его замыкание имеет конечный ранг в M.

LaTeX

$$$ \\operatorname{IsRkFinite}_M(X) \\rightarrow \\operatorname{IsRkFinite}_M\\bigl(\\operatorname{closure}_M(X)\\bigr)$$$

Lean4

theorem closure (h : M.IsRkFinite X) : M.IsRkFinite (M.closure X) :=
  let ⟨_, hI⟩ := M.exists_isBasis' X
  hI.isBasis_closure_right.isRkFinite_of_finite <| hI.finite_of_isRkFinite h

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