insert_not_isBase — Mathlib

English

Let M be a matroid on α and let B be a base of M. If e is an element not in B, then B ∪ {e} is not a base of M.

Русский

Пусть M — матроид на α и B — база M. Если e ∉ B, то B ∪ {e} не является базой M.

LaTeX

$$$\forall {\alpha} {M : Matroid \alpha} {B : Set \alpha} {e : \alpha}, M.IsBase B \to e \notin B \to \neg M.IsBase (B \cup \{e\})$$$

Lean4

theorem insert_not_isBase {e : α} (hB : M.IsBase B) (heB : e ∉ B) : ¬M.IsBase (insert e B) := fun h ↦
  h.not_isBase_of_ssubset (ssubset_insert heB) hB

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