subset_union_right

Mathlib.Data.Finset.Lattice.Basic

URI: https://scilib.ai/kg/mathlib#Finset.subset_union_right

English

Any subset T of S ∪ T is contained in the union; i.e., T ⊆ S ∪ T.

Русский

Любое подмножество T внутри S ∪ T удовлетворяет T ⊆ S ∪ T.

LaTeX

$$$ t \subseteq s \cup t $$$

Lean4

@[simp]
theorem subset_union_right : s₂ ⊆ s₁ ∪ s₂ := fun _ ↦ mem_union_right _

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

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

Разделы

Аффилиация

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