embDomain_notin_image_support — Mathlib

English

If b is not in the image of f applied to the support of x, then the coefficient at b of embDomain f x is zero.

Русский

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

LaTeX

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

Lean4

theorem embDomain_notin_image_support {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {b : Γ'} (hb : b ∉ f '' x.support) :
    (embDomain f x).coeff b = 0 :=
  dif_neg hb

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