sum_le_sum

Mathlib.SetTheory.Cardinal.Order

URI: https://scilib.ai/kg/mathlib#Cardinal.sum_le_sum

← MathLib Explorer

English

If f(i) ≤ g(i) for all i, then sum f ≤ sum g.

Русский

Если f(i) ≤ g(i) для всех i, то сумма f ≤ сумма g.

LaTeX

$$$\\forall i, f(i) \\le g(i) \\implies \\sum f \\le \\sum g$$$

Lean4

theorem sum_le_sum {ι} (f g : ι → Cardinal) (H : ∀ i, f i ≤ g i) : sum f ≤ sum g :=
  ⟨(Embedding.refl _).sigmaMap fun i =>
      Classical.choice <| by have := H i; rwa [← Quot.out_eq (f i), ← Quot.out_eq (g i)] at this⟩

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

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

Разделы

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

Аффилиация

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