embDomain_notin_range — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem embDomain_notin_range {f : Γ ↪o Γ'} {x : HahnSeries Γ R} {b : Γ'} (hb : b ∉ Set.range f) :
    (embDomain f x).coeff b = 0 :=
  embDomain_notin_image_support fun con => hb (Set.image_subset_range _ _ con)

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