map_succ — Mathlib

English

An order isomorphism preserves the successor operation: f(succ a) = succ(f(a)).

Русский

Упорядоченное изоморфизм сохраняет операцию successor: f(succ a) = succ(f(a)).

LaTeX

$$f(\operatorname{succ} a) = \operatorname{succ}(f(a))$$

Lean4

theorem _root_.OrderIso.map_succ [PartialOrder β] [SuccOrder β] (f : α ≃o β) (a : α) : f (succ a) = succ (f a) :=
  by
  by_cases h : IsMax a
  · rw [h.succ_eq, (f.isMax_apply.2 h).succ_eq]
  · exact (f.map_covBy.2 <| covBy_succ_of_not_isMax h).succ_eq.symm

Похожие утверждения