English
The preimage of a decidable order is decidable: if s is a decidable relation on β, then the induced order on α via f is decidable.
Русский
Образ обратного порядка детерминирован: если s — детерминированная отношение на β, то индукцированное отношение на α через f детерминировано.
LaTeX
$$$\\forall f:\\n\\alpha \\to \\beta,\\ \\forall s:\\beta \\to \\beta \\to \\mathrm{Prop},\\ \\mathrm{DecidableRel}(s) \\to \\mathrm{DecidableRel}(\\mathrm{Order.Preimage}(f,s))$$$
Lean4
/-- The preimage of a decidable order is decidable. -/
instance decidable (f : α → β) (s : β → β → Prop) [H : DecidableRel s] : DecidableRel (f ⁻¹'o s) := fun _ _ ↦ H _ _
