mulSupport_extend_one_subset — Mathlib

English

For any f,g, mulSupport (f.extend g 1) ⊆ f'' mulSupport g.

Русский

mulSupport(прикладывая f.extend g 1) ⊆ образ f от mulSupport g.

LaTeX

$$$ \\mathrm{mulSupport}(\\mathrm{extend}\\ f\\ g\\ 1) \\subseteq f''(\\mathrm{mulSupport}(g)) $$$

Lean4

@[to_additive]
theorem mulSupport_extend_one_subset {f : ι → κ} {g : ι → N} : mulSupport (f.extend g 1) ⊆ f '' mulSupport g :=
  mulSupport_subset_iff'.mpr fun x hfg ↦ by
    by_cases hf : ∃ a, f a = x
    · rw [extend, dif_pos hf, ← notMem_mulSupport]
      rw [← Classical.choose_spec hf] at hfg
      exact fun hg ↦ hfg ⟨_, hg, rfl⟩
    · rw [extend_apply' _ _ _ hf]; rfl

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