union_eq_union_iff_right

Mathlib.Data.Set.Basic

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

English

Let S, T, U be sets. If S ∪ U = T ∪ U, then S ⊆ T ∪ U and T ⊆ S ∪ U.

Русский

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

LaTeX

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

Lean4

theorem union_eq_union_iff_right : s ∪ u = t ∪ u ↔ s ⊆ t ∪ u ∧ t ⊆ s ∪ u :=
  sup_eq_sup_iff_right

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

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

Разделы

Аффилиация

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