cast_card_union

Mathlib.Data.Finset.CastCard

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

English

For s ⊆ t, (#(t \\ s) : R) = #t - #s.

Русский

Для s ⊆ t, (#(t \\ s) : R) = #t - #s.

LaTeX

$$$\\mathrm{cast}\\,( #(t \\ s) ) = #t - #s$$$

Lean4

theorem cast_card_union : (#(s ∪ t) : R) = #s + #t - #(s ∩ t) := by
  rw [eq_sub_iff_add_eq, ← cast_add, card_union_add_card_inter, cast_add]

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

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

Разделы

Аффилиация

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