card_union_le

Mathlib.Data.Finset.Card

URI: https://scilib.ai/kg/mathlib#Finset.card_union_le

English

For finite sets s,t, the cardinality of their union is at most the sum of their cardinalities.

Русский

Для конечных множеств s,t кардинальность их объединения не превосходит суммы кардинальностей.

LaTeX

$$|s ∪ t| ≤ |s| + |t|$$

Lean4

theorem card_union_le (s t : Finset α) : #(s ∪ t) ≤ #s + #t := by grind

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

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

Разделы

Аффилиация

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