exists_of_closure_ssubset — Mathlib

English

Let M be a matroid on α. If the closure of X is strictly contained in the closure of Y, then there exists an element e in Y that does not lie in the closure of X.

Русский

Пусть M — матроид на α. Если cl(X) ⊊ cl(Y), то существует элемент e ∈ Y, который не лежит в cl(X).

LaTeX

$$$\\operatorname{cl}(X) \subsetneq \\operatorname{cl}(Y) \\Rightarrow \\exists e \\in Y, e \\notin \\operatorname{cl}(X)$$$

Lean4

theorem exists_of_closure_ssubset (hXY : M.closure X ⊂ M.closure Y) : ∃ e ∈ Y, e ∉ M.closure X :=
  by
  by_contra! hcon
  exact hXY.not_subset (M.closure_subset_closure_of_subset_closure hcon)

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