sdiff_disjoint

Mathlib.Data.Finset.Basic

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

English

For any finite S,T, the sets T \\ S and S are disjoint: Disjoint (T \\ S) S.

Русский

Пусть S,T — конечные множества. Тогда T \\ S и S не пересекаются: Disjoint (T \\ S) S.

LaTeX

$$$\\operatorname{Disjoint}(T \\setminus S, S)$$$

Lean4

theorem sdiff_disjoint : Disjoint (t \ s) s :=
  disjoint_left.2 fun _a ha => (mem_sdiff.1 ha).2

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

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

Разделы

Аффилиация

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