English
There is a construction that pulls back a PartialOrder along an injective function, preserving ≤ and < relations and antisymmetry.
Русский
Существует конструкция переноса частичного порядка вдоль инъекции, сохраняющая отношения ≤ и < и антисимметрию.
LaTeX
$$$\text{PartialOrder on } α\text{ induced by } f: α → β \text{ via injective } f$$$
Lean4
/-- Pull back a `PartialOrder` instance along an injective function.
See note [reducible non-instances]. -/
abbrev partialOrder [PartialOrder β] [LE α] [LT α] (f : α → β) (hf : Function.Injective f)
(le : ∀ {x y}, f x ≤ f y ↔ x ≤ y) (lt : ∀ {x y}, f x < f y ↔ x < y) : PartialOrder α
where
__ := Function.Injective.preorder f le lt
le_antisymm _ _ h₁ h₂ := hf <| le_antisymm (le.2 h₁) (le.2 h₂)
