isRkFinite_closure_iff — Mathlib

English

Let M be a matroid on α. X has finite rank in M if and only if its closure has finite rank in M.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem isRkFinite_closure_iff : M.IsRkFinite (M.closure X) ↔ M.IsRkFinite X :=
  by
  rw [← isRkFinite_inter_ground_iff (X := X)]
  exact ⟨fun h ↦ h.subset <| M.inter_ground_subset_closure X, fun h ↦ by simpa using h.closure⟩

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