eRk_insert_eq_add_one — Mathlib

English

If e is a non-closure element outside X, then inserting e into X increases the rank by exactly one: eRk(insert e X) = eRk X + 1.

Русский

Если e не вclosure(X), добавление e в X увеличивает ранг ровно на единицу.

LaTeX

$$$(e \\in M.E \\setminus M.closure X) \\Rightarrow M.eRk(\\operatorname{insert} e X) = M.eRk X + 1$$$

Lean4

theorem eRk_insert_eq_add_one (he : e ∈ M.E \ M.closure X) : M.eRk (insert e X) = M.eRk X + 1 :=
  by
  obtain ⟨I, hI⟩ := M.exists_isBasis' X
  rw [← hI.closure_eq_closure, mem_diff, hI.indep.mem_closure_iff', not_and] at he
  rw [← eRk_closure_eq, ← closure_insert_congr_right hI.closure_eq_closure, hI.eRk_eq_encard, eRk_closure_eq,
    Indep.eRk_eq_encard (by tauto), encard_insert_of_notMem (by tauto)]

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