union_inter_cancel_right

Mathlib.Data.Set.Basic

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

English

The union with an intersection cancels on the right: (S ∪ T) ∩ T = T.

Русский

Объединение и пересечение справа взаимно сокращаются: (S ∪ T) ∩ T = T.

LaTeX

$$(S \cup T) \cap T = T$$

Lean4

theorem union_inter_cancel_right {s t : Set α} : (s ∪ t) ∩ t = t :=
  inter_eq_self_of_subset_right subset_union_right

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

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

Разделы

Аффилиация

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