hasProd_map_iff — Mathlib

English

If g is injective and a certain condition holds, then HasProd (f ∘ g) a (L.comap ⟨g,hg⟩) is equivalent to HasProd f a L.

Русский

Если 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_map_iff {L : SummationFilter γ} {g : γ → β} (hg : Injective g) :
    HasProd f a (L.map ⟨g, hg⟩) ↔ HasProd (f ∘ g) a L := by simp [HasProd, Function.comp_def]

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