instDiscreteTopologyOfFiniteOfJacobsonSpace

English

If X is finite and Jacobson, then X has the discrete topology.

Русский

Если X конечен и является пространством Якобсона, то у него дискретная топология.

LaTeX

$$$\text{Finite}(X) \land \operatorname{JacobsonSpace}(X) \Rightarrow \operatorname{DiscreteTopology}(X)$$$

Lean4

instance (priority := 100) [Finite X] [JacobsonSpace X] : DiscreteTopology X :=
  JacobsonSpace.discreteTopology (Set.toFinite _)

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