trans

Mathlib.SetTheory.Lists

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

← MathLib Explorer

English

If l1 ⊆ l2 and l2 ⊆ l3, then l1 ⊆ l3.

Русский

Если l1 ⊆ l2 и l2 ⊆ l3, то l1 ⊆ l3.

LaTeX

$$$l_1 \\subseteq l_2 \\land l_2 \\subseteq l_3 \\Rightarrow l_1 \\subseteq l_3$$$

Lean4

theorem trans {l₁ l₂ l₃ : Lists' α true} (h₁ : l₁ ⊆ l₂) (h₂ : l₂ ⊆ l₃) : l₁ ⊆ l₃ :=
  subset_def.2 fun _ m₁ => mem_of_subset h₂ <| mem_of_subset' h₁ m₁

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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