instHasSSubset

Mathlib.Data.Set.Basic

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

English

The strict-subset relation on Set α is the canonical order relation.

Русский

Строгое включение ⊂ на множестве подмножеств задаёт порядковую связь.

LaTeX

$$$\\text{HasSSubset}(\\mathrm{Set}(\\alpha))$ реализуется через $\\subset$ как строгую подмножество.$$

Lean4

instance : HasSSubset (Set α) :=
  ⟨(· < ·)⟩

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

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

Разделы

Аффилиация

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