supSpanSingleton_apply_mk — Mathlib

English

For mkSpanSingletonx y hx, the value at x′ with hx′ holds equals f(x′) + c y.

Русский

Для mkSpanSingleton x y hx, значение на x′ равно f(x′) + c y.

LaTeX

$$$$ f^{\\mathrm{supSpanSingleton}}(x,y,hx)\\;\\langle x'+c x, \\ldots\\rangle = f( x') + c y, $$$$

Lean4

@[simp]
theorem supSpanSingleton_apply_mk (f : E →ₗ.[K] F) (x : E) (y : F) (hx : x ∉ f.domain) (x' : E) (hx' : x' ∈ f.domain)
    (c : K) :
    f.supSpanSingleton x y hx ⟨x' + c • x, mem_sup.2 ⟨x', hx', _, mem_span_singleton.2 ⟨c, rfl⟩, rfl⟩⟩ =
      f ⟨x', hx'⟩ + c • y :=
  by
  unfold supSpanSingleton
  rw [sup_apply _ ⟨x', hx'⟩ ⟨c • x, _⟩, mkSpanSingleton'_apply]
  · rfl
  · exact mem_span_singleton.2 ⟨c, rfl⟩

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