Localic completion of generalized metric spaces II: Powerlocales

by STEVEN VICKERS

The finite powerset of a set. We show that in the presence of a Fintype it is the same as the ordinary powerset, and in the case of ℕ, ℚ, ℝ, ℂ it is not the same.

def setSetFin (X : Type u_1) : Set (Set X)

Equations

• setSetFin X = {A : Set X | A.Finite}

def setSetUniv (X : Type u_1) : Set (Set X)

Equations

• setSetUniv X = Set.univ

def powersetUniv (X : Type u_1) : Set (Set X)

Equations

• powersetUniv X = 𝒫 Set.univ

theorem finite_powerset_improper {X : Type u_1} [Infinite X] : setSetFin X ≠ setSetUniv X

The finite powerset of an infinite set X is distinct from the powerset of X.

instance instInfiniteReal_marginis : Infinite ℝ

There are infinitely many real numbers.

Equations

• instInfiniteReal_marginis = ⋯

instance instInfiniteComplex_marginis : Infinite ℂ

There are infinitely many complex numbers.

Equations

• instInfiniteComplex_marginis = ⋯