English
PredOrder transfers across order isomorphisms: if X ≃o Y, then Y inherits a PredOrder by transporting pred via the isomorphism.
Русский
PredOrder переносится через изоморфизм порядка: если X ≃o Y, то Y наследует PredOrder, переносив pred через изоморфизм.
LaTeX
$$$$ \operatorname{PredOrder}(Y) \text{ defined by } \operatorname{pred}(y) = f(\\operatorname{pred}(f^{-1}(y))). $$$$
Lean4
/-- `PredOrder` transfers across equivalences between orders. -/
protected abbrev ofOrderIso [PredOrder X] (f : X ≃o Y) : PredOrder Y
where
pred y := f (pred (f.symm y))
pred_le y := by rw [← le_map_inv_iff f]; exact pred_le (f.symm y)
min_of_le_pred
h := by
rw [← f.symm.isMin_apply]
refine min_of_le_pred ?_
simp [f.symm_apply_le, h]
le_pred_of_lt h := by rw [← map_inv_le_iff]; exact le_pred_of_lt (by simp [h])
