support_embDomain_subset — Mathlib

English

If b is not in the range of f, then the coefficient at b of embDomain f x is zero.

Русский

Если b не находится в диапазоне отображения f, то коэффициент в embDomain f x при b равен нулю.

LaTeX

$$$ (\\mathrm{embDomain} f\\,x).\\mathrm{coeff}(b) = 0 \\quad\\text{if } b \\notin \\operatorname{range}(f) $$

Lean4

theorem support_embDomain_subset {f : Γ ↪o Γ'} {x : HahnSeries Γ R} : support (embDomain f x) ⊆ f '' x.support :=
  by
  intro g hg
  contrapose! hg
  rw [mem_support, embDomain_notin_image_support hg, Classical.not_not]

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