diff_eq

Mathlib.Data.Set.Operations

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

English

For sets s,t, s \\ t equals s ∩ t^c.

Русский

Для множеств s,t множества s \\ t равно s ∩ t^c.

LaTeX

$$$s \\ t = s \\cap t^{c}$$$

Lean4

theorem diff_eq (s t : Set α) : s \ t = s ∩ tᶜ :=
  rfl

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

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

Разделы

Аффилиация

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