English
If α is a linear order with OrderClosedTopology and is both PredOrder and SuccOrder, then α carries the discrete topology.
Русский
Если α — линейный порядок с OrderClosedTopology и является PredOrder и SuccOrder, то он имеет дискретную топологию.
LaTeX
$$$ \\text{DiscreteTopology}(\\alpha) \\quad\\text{при } [PredOrder(\\alpha)] \\land [SuccOrder(\\alpha)]. $$$
Lean4
/-- The only order closed topology on a linear order which is a `PredOrder` and a `SuccOrder`
is the discrete topology.
This theorem is not an instance,
because it causes searches for `PredOrder` and `SuccOrder` with their `Preorder` arguments
and very rarely matches. -/
theorem of_predOrder_succOrder [PredOrder α] [SuccOrder α] : DiscreteTopology α :=
by
refine discreteTopology_iff_nhds.mpr fun a ↦ ?_
rw [← nhdsWithin_univ, ← Iic_union_Ioi, nhdsWithin_union, PredOrder.nhdsLE, SuccOrder.nhdsGT, sup_bot_eq]
