disjoint_sdiff_inter

Mathlib.Order.BooleanAlgebra.Set

URI: https://scilib.ai/kg/mathlib#Set.disjoint_sdiff_inter

English

Disjoint (s \\ t) and (s ∩ t).

Русский

Разность и пересечение множества s — несовместны.

LaTeX

$$$ (s \\\\setminus t) \\\\cap (s \\\\cap t) = \\\\emptyset $$$

Lean4

theorem disjoint_sdiff_inter : Disjoint (s \ t) (s ∩ t) :=
  disjoint_of_subset_right inter_subset_right disjoint_sdiff_left

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

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

Разделы

Аффилиация

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