height_orderIso — Mathlib

English

If f is an order isomorphism, then height(f(x)) = height(x) for all x.

Русский

Если f — перестановка порядка, тогда height(f(x)) = height(x) для всех x.

LaTeX

$$$ height(f(x)) = height(x) $$$

Lean4

@[simp]
theorem height_orderIso (f : α ≃o β) (x : α) : height (f x) = height x :=
  by
  apply le_antisymm
  · simpa using height_le_height_apply_of_strictMono _ f.symm.strictMono (f x)
  · exact height_le_height_apply_of_strictMono _ f.strictMono x

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