mkSpanSingleton'_apply — Mathlib

English

For any x,y,H,c,h as in the definition, mkSpanSingleton' x y H mapped on ⟨c·x,h⟩ equals c·y.

Русский

Для любых x,y,H,c,h из определения, mkSpanSingleton' x y H, применяемое к ⟨c·x,h⟩, равно c·y.

LaTeX

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

Lean4

@[simp]
theorem mkSpanSingleton'_apply (x : E) (y : F) (H : ∀ c : R, c • x = 0 → c • y = 0) (c : R) (h) :
    mkSpanSingleton' x y H ⟨c • x, h⟩ = c • y :=
  by
  dsimp [mkSpanSingleton']
  rw [← sub_eq_zero, ← sub_smul]
  apply H
  simp only [sub_smul, sub_eq_zero]
  apply Classical.choose_spec (mem_span_singleton.1 h)

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