supSpanSingleton_apply_self — Mathlib

English

The partial map built from supSpanSingleton with c = 1 returns y on the added vector x.

Русский

Частичное отображение, полученное через supSpanSingleton с коэффициентом 1, отдаёт y на добавляемом векторе x.

LaTeX

$$$$ f^{\\mathrm{supSpanSingleton}} x = y. $$$$

Lean4

@[simp]
theorem supSpanSingleton_apply_self (f : E →ₗ.[K] F) {x : E} (y : F) (hx : x ∉ f.domain) :
    f.supSpanSingleton x y hx ⟨x, mem_sup_right <| mem_span_singleton_self _⟩ = y := by
  simpa using supSpanSingleton_apply_smul_self f y hx 1

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