mkFinite — Mathlib

English

A finite discrete space yields a Stonean object via mkFinite.

Русский

Конечное дискретное пространство образует Stonean через конструктор mkFinite.

LaTeX

$$$\text{Stonean.mkFinite}(X) \in \text{Stonean}$$$

Lean4

/-- A finite discrete space as a Stonean space.
-/
def mkFinite (X : Type*) [Finite X] [TopologicalSpace X] [DiscreteTopology X] : Stonean
    where
  toTop := (CompHaus.of X).toTop
  prop := by
    dsimp
    constructor
    intro U _
    apply isOpen_discrete (closure U)

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