instIsTransSSubset

Mathlib.Data.Finset.Defs

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

English

Transitivity of strict subset: if s ⊂ t and t ⊂ u then s ⊂ u.

Русский

Транзитивность строгого подмножества: если s ⊂ t и t ⊂ u, то s ⊂ u.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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