extend_apply_self — Mathlib

English

For any hs and x in the extended submodule, the basis construction applied to x yields the same x when viewed as an element of the ambient module.

Русский

Для любых hs и x из расширенного подпространства конструирование базиса даёт тот же самый элемент x, если рассматривать как элемент исходного модуля.

LaTeX

$$$\\text{extend hs hst ht}\\; x = x$$$

Lean4

theorem extend_apply_self (hs : LinearIndepOn K id s) (x : hs.extend _) : Basis.extend hs x = x :=
  Basis.mk_apply _ _ _

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