finite_of_compactSpace_of_t2Space

English

Compact Hausdorff topological fields are finite; in particular, a compact, T2 topological division ring has finitely many elements.

Русский

Компактные и эргодические поля с топологией Гаусдорфа конечны; в частности, у компактного T2 топологического деления кольца конечное число элементов.

LaTeX

$$Finite K$$

Lean4

/-- Compact Hausdorff topological fields are finite. This is not an instance, as it would apply to
every `Finite` goal, causing slowly failing typeclass search in some cases. -/
theorem finite_of_compactSpace_of_t2Space {K} [DivisionRing K] [TopologicalSpace K] [IsTopologicalRing K]
    [CompactSpace K] [T2Space K] : Finite K :=
  by
  suffices DiscreteTopology K by exact finite_of_compact_of_discrete
  rw [discreteTopology_iff_isOpen_singleton_zero]
  exact GroupWithZero.isOpen_singleton_zero

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