embDomain_apply — Mathlib

English

Applying an embedding to a summable family yields the corresponding embedded domain element, with zeros outside the range.

Русский

Применение вложения к суммируемому семейству даёт соответствующий элемент домена-вложения, нули вне диапазона.

LaTeX

$$$ s.embDomain f b = \text{if } b \in \mathrm{range}\, f \text{ then } s (\mathrm{choose} (range\_mem\_range f)) else 0 $$$

Lean4

theorem embDomain_apply : s.embDomain f b = if h : b ∈ Set.range f then s (Classical.choose h) else 0 :=
  rfl

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