of_linearLocallyFinite — Mathlib

English

Let α be a linearly ordered set with LocallyFiniteOrder and a discrete topology. Then α carries an order topology, and this order topology coincides with the given discrete topology.

Русский

Пусть α имеет линейный порядок, локально конечный порядок и дискретную топологию. Тогда на α определяется топология порядка, которая совпадает с данной дискретной топологией.

LaTeX

$$$\\mathcal{T}_{\\mathrm{ord}}(\\alpha) = \\mathcal{D}(\\alpha)\\;\\text{for } (\\alpha, \\le) \\text{ linear and LocallyFiniteOrder, DiscreteTopology }$$$

Lean4

instance of_linearLocallyFinite [LinearOrder α] [LocallyFiniteOrder α] [DiscreteTopology α] : OrderTopology α :=
  haveI := LinearLocallyFiniteOrder.succOrder α
  haveI := LinearLocallyFiniteOrder.predOrder α
  inferInstance

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