summable_comp_injective

Mathlib.Topology.Instances.NNReal.Lemmas

URI: https://scilib.ai/kg/mathlib#NNReal.summable_comp_injective

← MathLib Explorer

English

If a function f is summable and i is injective, then f∘i is summable.

Русский

Если f суммируема и i инъективна, то f∘i суммируема.

LaTeX

$$Summable(f) → Injective(i) → Summable(f ∘ i)$$

Lean4

theorem summable_comp_injective {β : Type*} {f : α → ℝ≥0} (hf : Summable f) {i : β → α} (hi : Function.Injective i) :
    Summable (f ∘ i) := by
  rw [← summable_coe] at hf ⊢
  exact hf.comp_injective hi

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru