le_sum

Mathlib.SetTheory.Cardinal.Order

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

← MathLib Explorer

English

For any family f: ι → Cardinal and any i, f(i) ≤ sum f.

Русский

Для любой семейства f: ι → Cardinal и любого i, выполняется f(i) ≤ сумма f.

LaTeX

$$$f(i) \\le \\sum f$$$

Lean4

theorem le_sum {ι} (f : ι → Cardinal) (i) : f i ≤ sum f :=
  by
  rw [← Quotient.out_eq (f i)]
  exact ⟨⟨fun a => ⟨i, a⟩, fun a b h => by injection h⟩⟩

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

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

Разделы

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

Аффилиация

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