hasProd_iff_of_mulSupport — Mathlib

English

Let e be an equivalence between mulSupport f and mulSupport g, and assume the pointwise correspondence between g and f through e. Then HasProd f a ↔ HasProd g a.

Русский

Пусть e — эквивалент между mulSupport f и mulSupport g, и существует соответствие значений g через e: HasProd f a ↔ HasProd g a.

LaTeX

$$$e:\; mulSupport f \simeq mulSupport g\;\land\; (\forall x, g (e x) = f x) \Rightarrow HasProd f a \iff HasProd g a$$

Lean4

@[to_additive]
theorem hasProd_iff_of_mulSupport {g : γ → α} (e : mulSupport f ≃ mulSupport g)
    (he : ∀ x : mulSupport f, g (e x) = f x) : HasProd f a ↔ HasProd g a :=
  by
  have : (g ∘ (↑)) ∘ e = f ∘ (↑) := funext he
  rw [← hasProd_subtype_mulSupport, ← this, e.hasProd_iff, hasProd_subtype_mulSupport]

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