union_eq_union_iff_left

Mathlib.Data.Set.Basic

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

English

Let S, T, U be subsets of a common universe. If S ∪ T = S ∪ U, then T ⊆ S ∪ U and U ⊆ S ∪ T.

Русский

Пусть S, T, U — множества. Если S ∪ T = S ∪ U, то T ⊆ S ∪ U и U ⊆ S ∪ T.

LaTeX

$$$S \cup T = S \cup U \iff T \subseteq S \cup U \land U \subseteq S \cup T$$$

Lean4

theorem union_eq_union_iff_left : s ∪ t = s ∪ u ↔ t ⊆ s ∪ u ∧ u ⊆ s ∪ t :=
  sup_eq_sup_iff_left

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

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

Разделы

Аффилиация

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