embDomain_notin_range — Mathlib

English

Let s be a summable family and f an embedding. If b lies outside the image of f, then the embedded domain value at b is zero: (s.embDomain f) b = 0 whenever b ∉ range f.

Русский

Пусть s — суммируемая семейство и f — вложение. Если b не принадлежит образу f, то соответствующий элемент в s.embDomain f равен нулю: (s.embDomain f) b = 0, если b ∉ range f.

LaTeX

$$$\forall s : HahnSeries.SummableFamily Γ R α$, $f : α \hookrightarrow β$, $b : β$, \; b \notin \operatorname{range} f \; \Rightarrow \; (s.embDomain f) b = 0$$$

Lean4

@[simp]
theorem embDomain_notin_range (h : b ∉ Set.range f) : s.embDomain f b = 0 := by rw [embDomain_apply, dif_neg h]

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