Source / pinned edition
mathlib.order
Source of package mathlib.order · sha256:37a4a1585b83e01fd4b3ad85e8b4d5a7748f38d80960568f9f2c8fba45774d2e
- work
- urn:arxo:mathlib.order#Import_Source_287aaacefdd9ec45f2cbdbff6927faf3b376c817c34afd744c76b912153f6da0
- number
- sha256:37a4a1585b83e01fd4b3ad85e8b4d5a7748f38d80960568f9f2c8fba45774d2e
- kind
- urn:arxo:mathlib.order#treatise
Import_Edition_287aaacefdd9ec45f2cbdbff6927faf3b376c817c34afd744c76b912153f6da0
- edition
- urn:arxo:mathlib.order#Import_Edition_287aaacefdd9ec45f2cbdbff6927faf3b376c817c34afd744c76b912153f6da0
- language
- en
- officiality
- official
- materialisation
- PINNED_OFFICIAL_BYTES
- life cycle
- —
Publications
| URI | Type | documentHash | Retrieved |
|---|---|---|---|
| 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 |
Fragments — 3
le_trans · lemma · referenced by: 1
en · official · sha256:61f42419a962dc3a7cb1c0902f6280f1b8c9fd0f064daa860a71f21eaf479723
/-- The relation `≤` on a preorder is transitive. -/
lemma le_trans : a ≤ b → b ≤ c → a ≤ c := Preorder.le_trans _ _ _Referencing norms: Import_Rule_45030394b40076410bd1334e2484ec6ef2c5dc46054fff2e6e61b63b0d3be99d
le_of_lt · lemma · referenced by: 1
en · official · sha256:18a6839d929dea25e815531a013927461c8c2655b157744e4d87bcb8db0645df
@[to_dual self] lemma le_of_lt (hab : a < b) : a ≤ b := (lt_iff_le_not_ge.1 hab).1Referencing norms: Import_Rule_65b6ecbfa5036509e4685321bf5478f566880e1b5f45e091a8b4bfe4d1134945
PartialOrder.toPreorder · defn · referenced by: 1
en · official · sha256:bf0c46b98b287989aa08deb41a0847b14f22fb58bebf6b256de1dbeb05969e3c
class PartialOrder (α : Type*) extends Preorder α where
protected le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = bReferencing norms: Import_Rule_bb8dac886fd22637fdc265b0fba534cd13e058077172a5e831175b34e6e7c5aa
The hash beside the text is the sha256 of its exact bytes. It is the check that the text shown matches the one pinned in the package: a divergence fails the oracle’s static analysis.