POWER SET

-type constructs the power set of a type, the set of all subsets, foundational for defining -algebras and measurable spaces in analysis. It extends set theory into type theory with a higher-level construct.

In this system, supports and operations, providing the domain for Lebesgue and custom measures.

Formation

(-Formation). The power set of a type is the set of all subsets of , typed as .

type exp =
  | Power of exp  (* P(A) *)

Introduction

(-Introduction). The power set is introduced as the collection of all possible sets .

let power_set (a : exp) : exp =
  Power (a)

Elimination

(-Elimination). Membership in holds for any set , allowing use in -algebras or measures.

let infer env ctx (Power a) =
  check env ctx a U; Set (Set a)

Computation

(-Computation). does not reduce directly but defines a type for subsets, verifiable via for equality.

let subset (s : exp) (a : exp) =
  Forall ("x", a, Implies (App (s, Var "x"), True))

Uniqueness

(-Uniqueness). The power set is unique for a given , containing all subsets and equal to another if .

let equal env ctx (Power a1) (Power a2) =
  equal env ctx a1 a2

Theorems

(Cardinality). For a finite type with elements, has elements, though infinite in cases like .

(Sigma-Algebra Basis). serves as the -algebra for the Lebesgue measure, containing all measurable subsets.

let lebesgue_sigma = Power (Set Real)