hasProd_comap_iff_of_hasSupport — Mathlib

English

Given injective g and a compatibility condition on f outside the range of g, HasProd (f ∘ g) a (L.comap ⟨g,hg⟩) iff HasProd f a L.

Русский

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

LaTeX

$$$ HasProd (f \circ g) a (L.comap { toFun := g, inj' := hg }) \leftrightarrow HasProd f a L $$$

Lean4

@[to_additive]
theorem hasProd_comap_iff_of_hasSupport [L.HasSupport] {g : γ → β} (hg : Injective g)
    (hf : ∀ x ∈ L.support, 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' ?_
  filter_upwards [L.eventually_le_support] with s hs
  rw [s.prod_preimage]
  exact fun x h h' ↦ hf x (hs h) h'

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