embDomain_single — Mathlib

English

The embedding map sends a Hahn series supported at a single index g to the Hahn series supported at f(g) with the same coefficient.

Русский

Отображение embDomain переводит Hahn-ряд, чья опорa состоит из одного индекса g, в Hahn-ряд с опорой на f(g) и тем же коэффициентом.

LaTeX

$$$ embDomain\;f\; (single\; g\; r) = single\; (f\;g)\; r $$$

Lean4

@[simp]
theorem embDomain_single {f : Γ ↪o Γ'} {g : Γ} {r : R} : embDomain f (single g r) = single (f g) r :=
  by
  ext g'
  by_cases h : g' = f g
  · simp [h]
  rw [embDomain_notin_image_support, coeff_single_of_ne h]
  by_cases hr : r = 0
  · simp [hr]
  rwa [support_single_of_ne hr, Set.image_singleton, Set.mem_singleton_iff]

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