discreteTopology_iff_orderTopology_of_pred_succ

English

For a linear order α with PredOrder and SuccOrder, the discrete topology on α is equivalent to the order topology.

Русский

Для линейного порядка α с предшественником и последователем дискретная топология на α эквивалентна топологии порядка.

LaTeX

$$DiscreteTopology α ↔ OrderTopology α$$

Lean4

theorem discreteTopology_iff_orderTopology_of_pred_succ [LinearOrder α] [PredOrder α] [SuccOrder α] :
    DiscreteTopology α ↔ OrderTopology α :=
  by
  refine ⟨fun h ↦ ⟨?_⟩, fun h ↦ .of_predOrder_succOrder⟩
  rw [h.eq_bot, LinearOrder.bot_topologicalSpace_eq_generateFrom]

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