English
SuccOrder transfers across order isomorphisms: if X ≃o Y, then Y inherits a SuccOrder by transporting succ via the isomorphism.
Русский
SuccOrder переносится через изоморфизмы порядка: если X ≃o Y, то Y наследует SuccOrder, перенося операцию succ через изоморфизм.
LaTeX
$$$$ \operatorname{SuccOrder}(Y) \text{ defined by } \operatorname{succ}(y) = f(\\operatorname{succ}(f^{-1}(y))), \ \ldots $$$$
Lean4
/-- `SuccOrder` transfers across equivalences between orders. -/
protected abbrev ofOrderIso [SuccOrder X] (f : X ≃o Y) : SuccOrder Y
where
succ y := f (succ (f.symm y))
le_succ y := by rw [← map_inv_le_iff f]; exact le_succ (f.symm y)
max_of_succ_le
h := by
rw [← f.symm.isMax_apply]
refine max_of_succ_le ?_
simp [f.le_symm_apply, h]
succ_le_of_lt
h := by rw [← le_map_inv_iff];
exact
succ_le_of_lt
(by simp [h])
-- See note [reducible non-instances]
