partialOrder

Mathlib.Data.Semiquot

URI: https://scilib.ai/kg/mathlib#Semiquot.partialOrder

Lean4

instance partialOrder : PartialOrder (Semiquot α)
    where
  le s t := ∀ ⦃x⦄, x ∈ s → x ∈ t
  le_refl _ := Set.Subset.refl _
  le_trans _ _ _ := Set.Subset.trans
  le_antisymm _ _ h₁ h₂ := ext_s.2 (Set.Subset.antisymm h₁ h₂)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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