subset_closure — Mathlib

English

Let M be a matroid and I a basis for X. Then every element of X lies in the closure of I, i.e. X ⊆ cl(I).

Русский

Пусть M — матроид, и I базис X. Тогда каждый элемент X принадлежит замыканию I, то есть X ⊆ cl(I).

LaTeX

$$$X \subseteq \operatorname{cl}(I)$$$

Lean4

theorem subset_closure (h : M.IsBasis I X) : X ⊆ M.closure I := by
  rw [← closure_subset_closure_iff_subset_closure, h.closure_eq_closure]

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