ordConnected_range — Mathlib

English

If e is an order isomorphism between α and β, then the range of e is OrdConnected.

Русский

Если e — порядок-изоморфизм между α и β, то образ e есть OrdConnected.

LaTeX

$$$\\operatorname{OrdConnected}(\\operatorname{range}(e))$$$

Lean4

@[instance]
theorem ordConnected_range {E : Type*} [EquivLike E α β] [OrderIsoClass E α β] (e : E) : OrdConnected (range e) :=
  by
  simp_rw [← image_univ]
  exact ordConnected_image (e : α ≃o β)

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