embDomain_some_some — Mathlib

English

Applying some to the embedded domain recovers the original finsupp: (f.embDomain .some).some = f.

Русский

Применение some к встроенной области восстанавливает исходную функцию: (f.embDomain .some).some = f.

LaTeX

$$$ (f.embDomain \.text{some}).text{some} = f $$$

Lean4

@[simp]
theorem embDomain_some_some [Zero M] (f : α →₀ M) (x) : f.embDomain .some (.some x) = f x := by
  simp [← Function.Embedding.some_apply]

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