hasProd_iff — Mathlib

English

If g is an inducing map between topological spaces, then HasProd (g ∘ f) (g a) L is equivalent to HasProd f a L for any f and a.

Русский

Если g — индукционный переход между топологическими пространствами, тогда HasProd (g ∘ f) (g a) L эквивалентно HasProd f a L для любых f и a.

LaTeX

$$$\text{IsInducing } g \Rightarrow (\text{HasProd } (g\circ f) (g a) L \iff \text{HasProd } f a L)$$$

Lean4

@[to_additive]
protected theorem hasProd_iff [CommMonoid γ] [TopologicalSpace γ] {G} [FunLike G α γ] [MonoidHomClass G α γ] {g : G}
    (hg : IsInducing g) (f : β → α) (a : α) : HasProd (g ∘ f) (g a) L ↔ HasProd f a L :=
  by
  simp_rw [HasProd, comp_apply, ← map_prod]
  exact hg.tendsto_nhds_iff.symm

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