union_eq_self_of_subset_right

Mathlib.Data.Set.Basic

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

English

If t ⊆ s then s ∪ t = s.

Русский

Если t ⊆ s, то s ∪ t = s.

LaTeX

$$$t \subseteq s \Rightarrow s \cup t = s$$$

Lean4

theorem union_eq_self_of_subset_right {s t : Set α} (h : t ⊆ s) : s ∪ t = s :=
  union_eq_left.mpr h

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

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

Разделы

Аффилиация

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