instTransSubsetSSubset

Mathlib.Data.Set.Basic

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

English

If S ⊆ T and T ⊂ U, then S ⊂ U.

Русский

Если S ⊆ T и T ⊂ U, то S ⊂ U.

LaTeX

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

Lean4

instance : Trans ((· ⊆ ·) : Set α → Set α → Prop) (· ⊂ ·) (· ⊂ ·) :=
  show Trans (· ≤ ·) (· < ·) (· < ·) by infer_instance

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

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

Разделы

Аффилиация

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