trans

Mathlib.Data.Set.Basic

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

English

If a ⊆ b and b ⊆ c, then a ⊆ c.

Русский

Если a ⊆ b и b ⊆ c, то a ⊆ c.

LaTeX

$$$\\forall a,b,c\\subseteq\\alpha, a\\subseteq b \\Rightarrow b\\subseteq c \\Rightarrow a\\subseteq c$$$

Lean4

@[trans]
theorem trans {a b c : Set α} (ab : a ⊆ b) (bc : b ⊆ c) : a ⊆ c := fun _ h => bc <| ab h

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

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

Разделы

Аффилиация

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