comp_injective — Mathlib

English

If f is Multipliable and i : γ → β is injective, then the composition f ∘ i is Multipliable.

Русский

Если f суммируема и i : γ → β — инъекция, тогда композиция f ∘ i суммируема.

LaTeX

$$$$\\text{Multipliable}(f) \\rightarrow \\text{Injective}(i) \\rightarrow \\text{Multipliable}(f \\circ i).$$$$

Lean4

@[to_additive]
theorem comp_injective {i : γ → β} (hf : Multipliable f) (hi : Injective i) : Multipliable (f ∘ i) := by
  simpa only [Set.mulIndicator_range_comp] using
    (hi.multipliable_iff (fun x hx ↦ Set.mulIndicator_of_notMem hx _)).2 (hf.mulIndicator (Set.range i))

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