English
There is a construction that pulls back a LinearOrder along an injective function, preserving ≤, <, and min/max/compare compatibilities.
Русский
Существует перенос линейного порядка вдоль инъекции, сохраняющий ≤, < и совместимость с min, max и compare.
LaTeX
$$$\text{LinearOrder on } α\text{ via injective } f: α \to β$ with preserved min, max, compare$$
Lean4
/-- Pull back a `LinearOrder` instance along an injective function.
See note [reducible non-instances]. -/
abbrev linearOrder [LinearOrder β] [LE α] [LT α] [Max α] [Min α] [Ord α] [DecidableEq α] [DecidableLE α] [DecidableLT α]
(f : α → β) (hf : Function.Injective f) (le : ∀ {x y}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y}, f x < f y ↔ x < y)
(min : ∀ x y, f (x ⊓ y) = f x ⊓ f y) (max : ∀ x y, f (x ⊔ y) = f x ⊔ f y)
(compare : ∀ x y, compare (f x) (f y) = compare x y) : LinearOrder α
where
toPartialOrder := hf.partialOrder _ le lt
toDecidableLE := ‹_›
toDecidableEq := ‹_›
toDecidableLT := ‹_›
le_total _ _ := by simp only [← le, le_total]
min_def _ _ := by simp_rw [← hf.eq_iff, ← le, apply_ite f, ← min_def, min]
max_def _ _ := by simp_rw [← hf.eq_iff, ← le, apply_ite f, ← max_def, max]
compare_eq_compareOfLessAndEq _
_ := by simp_rw [← compare, LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq, ← lt, hf.eq_iff]
