coe_extendLe — Mathlib

English

The extendLe construction is compatible with the ambient inclusion; its underlying function is the identity on the ambient space.

Русский

Конструкция extendLe совместима с включением в окружающее пространство; базисное отображение совпадает с тождественным на пространстве окружения.

LaTeX

$$$\\text{coe\_extendLe} : (Basis\\.extendLe\\ hs\\ hst\\ ht) = \\mathrm{id}$$$

Lean4

@[simp]
theorem coe_extendLe (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ span K t) :
    ⇑(Basis.extendLe hs hst ht) = ((↑) : _ → _) :=
  funext (extendLe_apply_self hs hst ht)

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