union_inter_cancel_right

Mathlib.Data.Finset.Lattice.Basic

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

English

The right cancellation: (S ∪ T) ∩ T = T.

Русский

Правое сокращение: (S ∪ T) ∩ T = T.

LaTeX

$$$(s \\cup t) \\cap t = t$$$

Lean4

@[simp]
theorem union_inter_cancel_right {s t : Finset α} : (s ∪ t) ∩ t = t := by grind

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

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

Разделы

Аффилиация

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