continuous — Mathlib

English

An order isomorphism between two linear order spaces with order topology is continuous.

Русский

Изоморфизм упорядочивания между двумя линейно упорядоченными пространствами с топологией порядка непрерывен.

LaTeX

$$$\\text{e : } \\alpha \\simeq_o \\beta \\Rightarrow \\text{Continuous } e.$$$

Lean4

protected theorem continuous (e : α ≃o β) : Continuous e :=
  by
  rw [‹OrderTopology β›.topology_eq_generate_intervals, continuous_generateFrom_iff]
  rintro s ⟨a, rfl | rfl⟩
  · rw [e.preimage_Ioi]
    apply isOpen_lt'
  · rw [e.preimage_Iio]
    apply isOpen_gt'

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