orderIso — Mathlib

English

Given an order embedding f: α ↪o β, there is an induced order isomorphism α ≃o Set.range f.

Русский

Для вложения порядка f: α ↪o β индуцируется изоморфизм порядка α ≃o Set.range f.

LaTeX

$$$\alpha \cong_o \mathrm{Set.range} f$$$

Lean4

/-- We can regard an order embedding as an order isomorphism to its range. -/
@[simps! apply]
noncomputable def orderIso [LE α] [LE β] {f : α ↪o β} : α ≃o Set.range f :=
  { Equiv.ofInjective _ f.injective with map_rel_iff' := f.map_rel_iff }

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