mulSupport_extend_one — Mathlib

English

If f is injective, mulSupport (extend f g 1) = f '' mulSupport g.

Русский

Если f инъективна, mulSupport extend f g 1 равно образ mulSupport g под f.

LaTeX

$$$ \\mathrm{mulSupport}(\\mathrm{extend}\\ f\\ g\\ 1) = \\mathrm{image}\\ f (\\mathrm{mulSupport}(g)) $$$

Lean4

@[to_additive]
theorem mulSupport_extend_one {f : ι → κ} {g : ι → N} (hf : f.Injective) :
    mulSupport (f.extend g 1) = f '' mulSupport g :=
  mulSupport_extend_one_subset.antisymm <| by rintro _ ⟨x, hx, rfl⟩; rwa [mem_mulSupport, hf.extend_apply]

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