pi_inter_compl

Mathlib.Data.Set.Prod

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

English

The pi-set over s, intersected with the pi-set over the complement s^c, equals the pi-set over the universal t.

Русский

Mножество π над s пересечено с π над s^c равно π над вселенским t.

LaTeX

$$$ \pi s t \cap \pi s^{c} t = \pi \; \mathrm{univ} \ t $$$

Lean4

@[simp]
theorem pi_inter_compl (s : Set ι) : pi s t ∩ pi sᶜ t = pi univ t := by grind

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

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

Разделы

Аффилиация

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