eRk_eq_eRk_insert — Mathlib

English

If I is a basis for X, then for any e, eRk(insert e I) = eRk(insert e X).

Русский

Если I базис X, то для любого элемента e выполняется eRk(вставить e в I) = eRk(вставить e в X).

LaTeX

$$$ (hIX : M.IsBasis I X) (e : α), M.eRk(\\insert e I) = M.eRk(\\insert e X) $$$

Lean4

theorem eRk_eq_eRk_insert (hIX : M.IsBasis I X) (e : α) : M.eRk (insert e I) = M.eRk (insert e X) := by
  rw [← union_singleton, hIX.eRk_eq_eRk_union, union_singleton]

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