disjSups_disjSups_disjSups_comm

Mathlib.Data.Finset.Sups

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

English

For Finsets s,t,u,v, s ○ t ○ (u ○ v) = s ○ u ○ (t ○ v).

Русский

Для Finset s,t,u,v верно s ○ t ○ (u ○ v) = s ○ u ○ (t ○ v).

LaTeX

$$$ s \\circ t \\circ (u \\circ v) = s \\circ u \\circ (t \\circ v) $$$

Lean4

theorem disjSups_disjSups_disjSups_comm : s ○ t ○ (u ○ v) = s ○ u ○ (t ○ v) := by
  simp_rw [← disjSups_assoc, disjSups_right_comm]

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

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

Разделы

Аффилиация

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