Источник / закреплённая редакция
mathlib.order
Источник пакета mathlib.order · sha256:37a4a1585b83e01fd4b3ad85e8b4d5a7748f38d80960568f9f2c8fba45774d2e
- work
- urn:arxo:mathlib.order#Import_Source_287aaacefdd9ec45f2cbdbff6927faf3b376c817c34afd744c76b912153f6da0
- номер
- sha256:37a4a1585b83e01fd4b3ad85e8b4d5a7748f38d80960568f9f2c8fba45774d2e
- вид
- urn:arxo:mathlib.order#treatise
Import_Edition_287aaacefdd9ec45f2cbdbff6927faf3b376c817c34afd744c76b912153f6da0
- edition
- urn:arxo:mathlib.order#Import_Edition_287aaacefdd9ec45f2cbdbff6927faf3b376c817c34afd744c76b912153f6da0
- язык
- en
- официальность
- official
- материализация
- PINNED_OFFICIAL_BYTES
- жизненный цикл
- —
Публикации
| URI | Тип | documentHash | Получено |
|---|---|---|---|
| https://github.com/leanprover-community/mathlib4/blob/db584cd6d46c92f209a44c0f1c829460d327499d/Mathlib/Order/Defs/PartialOrder.lean | text/plain; charset=utf-8 | sha256:324e420cd942d09b60b6ac8d662b01e29f13f0cd60513e2c4750b3e5676dcf46 | 2026-09-07T23:26:52Z |
Фрагменты — 3
le_trans · lemma · на него ссылаются: 1
en · official · sha256:61f42419a962dc3a7cb1c0902f6280f1b8c9fd0f064daa860a71f21eaf479723EN
/-- The relation `≤` on a preorder is transitive. -/
lemma le_trans : a ≤ b → b ≤ c → a ≤ c := Preorder.le_trans _ _ _Ссылаются нормы: Import_Rule_45030394b40076410bd1334e2484ec6ef2c5dc46054fff2e6e61b63b0d3be99d
le_of_lt · lemma · на него ссылаются: 1
en · official · sha256:18a6839d929dea25e815531a013927461c8c2655b157744e4d87bcb8db0645dfEN
@[to_dual self] lemma le_of_lt (hab : a < b) : a ≤ b := (lt_iff_le_not_ge.1 hab).1Ссылаются нормы: Import_Rule_65b6ecbfa5036509e4685321bf5478f566880e1b5f45e091a8b4bfe4d1134945
PartialOrder.toPreorder · defn · на него ссылаются: 1
en · official · sha256:bf0c46b98b287989aa08deb41a0847b14f22fb58bebf6b256de1dbeb05969e3cEN
class PartialOrder (α : Type*) extends Preorder α where
protected le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = bСсылаются нормы: Import_Rule_bb8dac886fd22637fdc265b0fba534cd13e058077172a5e831175b34e6e7c5aa
Хэш рядом с текстом — sha256 его точных байтов. Он и есть проверка того, что показанный текст совпадает с закреплённым в пакете: расхождение роняет статику оракула.