union_subset_union_right

Mathlib.Data.Set.Basic

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

English

s ∪ t1 ⊆ s ∪ t2 if t1 ⊆ t2.

Русский

s ∪ t1 ⊆ s ∪ t2 при условии t1 ⊆ t2.

LaTeX

$$$(s \cup t_1) \subseteq (s \cup t_2) \text{ при } t_1 \subseteq t_2$$$

Lean4

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

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

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

Разделы

Аффилиация

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