union_subset_union_left

Mathlib.Data.Set.Basic

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

English

If s1 ⊆ s2 then s1 ∪ t ⊆ s2 ∪ t.

Русский

Если s1 ⊆ s2, то s1 ∪ t ⊆ s2 ∪ t.

LaTeX

$$$s_1 \subseteq s_2 \Rightarrow (s_1 \cup t) \subseteq (s_2 \cup t)$$$

Lean4

theorem union_subset_union_left {s₁ s₂ : Set α} (t) (h : s₁ ⊆ s₂) : s₁ ∪ t ⊆ s₂ ∪ t :=
  union_subset_union h Subset.rfl

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

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

Разделы

Аффилиация

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