card_sdiff_eq_card_sdiff_iff

Mathlib.Data.Finset.Card

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

English

Let s and t be finite sets. Then |s \\ t| = |t \\ s| if and only if |s| = |t|.

Русский

Пусть s,t — конечные множества. Тогда |s \\ t| = |t \\ s| тогда и только тогда, когда |s| = |t|.

LaTeX

$$$|s \\setminus t| = |t \\setminus s| \\iff |s| = |t|$$$

Lean4

theorem card_sdiff_eq_card_sdiff_iff : #(s \ t) = #(t \ s) ↔ #s = #t := by grind

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

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

Разделы

Аффилиация

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