multipliable_iff — Mathlib

English

Let g: γ → β be an injective function and suppose f(x) = 1 for all x not in the range of g. Then Multipliable (f ∘ g) is equivalent to Multipliable f.

Русский

Пусть g: γ → β — инъекция и для всех x вне образа g выполняется f(x) = 1. Тогда Multipliable (f ∘ g) эквивалентно Multipliable f.

LaTeX

$$$\text{Injective } g\;\wedge\; (\forall x\notin \operatorname{range}(g),\ f(x)=1)\;\Rightarrow\; \text{Multipliable } (f\circ g) \iff \text{Multipliable } f$$$

Lean4

@[to_additive]
theorem multipliable_iff {g : γ → β} (hg : Injective g) (hf : ∀ x ∉ Set.range g, f x = 1) :
    Multipliable (f ∘ g) ↔ Multipliable f :=
  exists_congr fun _ ↦ hg.hasProd_iff hf

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