card_sdiff

Mathlib.Data.Finset.Card

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

English

For finite sets s,t, |t \ s| = |t| − |s ∩ t|.

Русский

Для конечных множеств s,t |t \ s| = |t| − |s ∩ t|.

LaTeX

$$|t \ s| = |t| − |s ∩ t|$$

Lean4

@[grind =]
theorem card_sdiff : #(t \ s) = #t - #(s ∩ t) := by rw [← card_sdiff_of_subset] <;> grind

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

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

Разделы

Аффилиация

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