subset_union_left

Mathlib.Data.Finset.Lattice.Basic

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

English

Any subset S of S ∪ T is just a subset of itself within the union; i.e., S ⊆ S ∪ T.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem subset_union_left : s₁ ⊆ s₁ ∪ s₂ := fun _ ↦ mem_union_left _

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

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

Разделы

Аффилиация

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