hasProd_extend_one — Mathlib

English

Let g: β → γ be injective. Then HasProd (extend g f 1) a is equivalent to HasProd f a; extending the index set by g and filling new coordinates with 1 does not affect the product convergence.

Русский

Пусть g: β → γ — инъекция. Тогда HasProd (extend g f 1) a эквивалентно HasProd f a; расширение индексов через g и заполнение новых координат единицей не меняют сходимость произведения.

LaTeX

$$$\text{Injective } g\;\Rightarrow\; \text{HasProd } (\text{extend } g\, f\, 1)\ a \iff \text{HasProd } f\ a$$$

Lean4

@[to_additive (attr := simp)]
theorem hasProd_extend_one {g : β → γ} (hg : Injective g) : HasProd (extend g f 1) a ↔ HasProd f a :=
  by
  rw [← hg.hasProd_iff, extend_comp hg]
  exact extend_apply' _ _

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