discreteTopology_bot — Mathlib

English

The discrete topology on α is the bottom element of the lattice of topologies; i.e., it is generated by the discrete base where every subset is open.

Русский

Дискретная топология на α является нижним элементом решетки топологий; то есть она порождается базой, где каждый подмножество открыто.

LaTeX

$$Bottom element equals DiscreteTopology: @DiscreteTopology α ⊥$$

Lean4

theorem discreteTopology_bot (α : Type*) : @DiscreteTopology α ⊥ :=
  @DiscreteTopology.mk α ⊥ rfl

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