mkSpanSingleton'_apply_self — Mathlib

English

Applying the span singleton to the base vector x yields y: mkSpanSingleton' x y H ⟨x, h⟩ = y.

Русский

Применение разложения на основание x возвращает y: mkSpanSingleton' x y H ⟨x,h⟩ = y.

LaTeX

$$$\\mathrm{mkSpanSingleton}'(x,y,H)\\langle x,h\\rangle = y$$$

Lean4

@[simp]
theorem mkSpanSingleton'_apply_self (x : E) (y : F) (H : ∀ c : R, c • x = 0 → c • y = 0) (h) :
    mkSpanSingleton' x y H ⟨x, h⟩ = y := by
  conv_rhs => rw [← one_smul R y]
  rw [← mkSpanSingleton'_apply x y H 1 ?_]
  · congr
    rw [one_smul]
  · rwa [one_smul]

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