supSpanSingleton_apply_of_mem — Mathlib

English

If x ∈ f.domain, then f.supSpanSingleton x y hx x' = f ⟨x', hx'⟩ for x' ∈ f.domain.

Русский

Если x принадлежит dom(f), то f.supSpanSingleton x y hx x' = f(x') для x'∈dom(f).

LaTeX

$$$$ f.supSpanSingleton x y hx x' = f \\langle x', hx' \\rangle $$$$

Lean4

theorem supSpanSingleton_apply_of_mem (f : E →ₗ.[K] F) {x : E} (y : F) (hx : x ∉ f.domain)
    (x' : (f.supSpanSingleton x y hx).domain) (hx' : (x' : E) ∈ f.domain) :
    f.supSpanSingleton x y hx x' = f ⟨x', hx'⟩ := by simpa using supSpanSingleton_apply_mk f x y hx x' hx' 0

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