eRk_insert_le_add_one — Mathlib

English

For any X and element e, inserting e into X increases the rank by at most one: eRk(insert e X) ≤ eRk(X) + 1.

Русский

Для любого X и элемента e добавление e в X увеличивает ранг не более чем на единицу: eRk(insert e X) ≤ eRk(X) + 1.

LaTeX

$$$M.eRk(\\operatorname{insert} e X) \\le M.eRk X + 1$$$

Lean4

theorem eRk_insert_le_add_one (M : Matroid α) (e : α) (X : Set α) : M.eRk (insert e X) ≤ M.eRk X + 1 :=
  union_singleton ▸ (M.eRk_union_le_eRk_add_eRk _ _).trans <| add_le_add_left (by simpa using M.eRk_le_encard { e }) _

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