hasProd_comap_iff — Mathlib

English

Without HasSupport assumptions, HasProd (f ∘ g) a (L.comap ⟨g,hg⟩) is equivalent to HasProd f a L for an injective g.

Русский

Без предположения HasSupport, HasProd(f ∘ g) a (L.comap ⟨g,hg⟩) эквивалентно HasProd f a L при инъективном g.

LaTeX

$$$ HasProd (f \circ g) a (L.comap ⟨g, hg⟩) \leftrightarrow HasProd f a L $$$

Lean4

@[to_additive]
theorem hasProd_comap_iff {g : γ → β} (hg : Injective g) (hf : ∀ x, x ∉ Set.range g → f x = 1) :
    HasProd (f ∘ g) a (L.comap ⟨g, hg⟩) ↔ HasProd f a L :=
  by
  simp only [HasProd, SummationFilter.comap_filter, tendsto_map'_iff, comp_apply, Embedding.coeFn_mk, Function.comp_def]
  refine tendsto_congr fun s ↦ ?_
  rw [s.prod_preimage]
  exact fun x _ h ↦ hf x h

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