trans

Mathlib.Data.Multiset.Defs

URI: https://scilib.ai/kg/mathlib#Multiset.Subset.trans

English

If s ⊆ t and t ⊆ u, then s ⊆ u.

Русский

Если s ⊆ t и t ⊆ u, то s ⊆ u.

LaTeX

$$$$s \subseteq t \rightarrow t \subseteq u \rightarrow s \subseteq u$$$$

Lean4

theorem trans {s t u : Multiset α} : s ⊆ t → t ⊆ u → s ⊆ u := fun h₁ h₂ _ m => h₂ (h₁ m)

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

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

Разделы

Аффилиация

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