bot_topologicalSpace_eq_generateFrom

English

In a linear order with predecessor and successor, the bottom topology equals the topology generated by the rays Ioi a and Iio a.

Русский

В линейном порядке с предшественником и преемником нижняя топология равна топологии, порождаемой полуоднями Ioi a и Iio a.

LaTeX

$$$(\perp : \text{TopologicalSpace } \alpha) = \ text{generateFrom} \{ s \mid \exists a, s = \mathrm{Ioi}(a) \lor s = \mathrm{Iio}(a) \}. $$$

Lean4

theorem bot_topologicalSpace_eq_generateFrom {α} [LinearOrder α] [PredOrder α] [SuccOrder α] :
    (⊥ : TopologicalSpace α) = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a} :=
  by
  let _ := Preorder.topology α
  have : OrderTopology α := ⟨rfl⟩
  exact DiscreteTopology.of_predOrder_succOrder.eq_bot.symm

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