map_top' — Mathlib

English

An order isomorphism maps the top element to the top, provided top exists in both domains.

Русский

Порядковый изоморфизм переводит максимальный элемент в максимальный, если они существуют в обеих областях.

LaTeX

$$$ f\,\top = \top $$$

Lean4

theorem map_top' [LE α] [PartialOrder β] (f : α ≃o β) {x : α} {y : β} (hx : ∀ x', x' ≤ x) (hy : ∀ y', y' ≤ y) :
    f x = y :=
  f.dual.map_bot' hx hy

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