instIsTransSSubset

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.instIsTransSSubset

English

If S ⊊ T and T ⊊ U, then S ⊊ U.

Русский

Если S ⊊ T и T ⊊ U, то S ⊊ U.

LaTeX

$$$\\forall S,T,U\\subseteq\\alpha, (S\\subset T) \\land (T\\subset U) \\Rightarrow (S\\subset U)$$$

Lean4

instance : IsTrans (Set α) (· ⊂ ·) :=
  show IsTrans (Set α) (· < ·) by infer_instance

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

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

Разделы

Аффилиация

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