encard_iUnion_le_of_fintype

Mathlib.Data.Set.Card.Arithmetic

URI: https://scilib.ai/kg/mathlib#Set.encard_iUnion_le_of_fintype

← MathLib Explorer

English

If ι is finite, then the encard of the union is at most the finsum of encards.

Русский

Если индексный тип конечен, encard объединения не превосходит суммы encard.

LaTeX

$$$(\\bigcup_i s(i)).encard \\le \\sum_i (s(i)).encard$$

Lean4

theorem encard_iUnion_le_of_fintype [Fintype ι] (s : ι → Set α) : (⋃ i, s i).encard ≤ ∑ i, (s i).encard := by
  simpa using Finset.univ.set_encard_biUnion_le s

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

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

Разделы

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

Аффилиация

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