INFINITE UNION

(Union). defines an infinite union over an indexed family of sets, foundational for -algebras and limits in analysis.

type exp =
  | Union of exp * exp  (* ⋃_i S_i *)

Rules

. (Intro). Introduced as , where is an index type (e.g., ) and is a family. Membership is , feeding into .

let infinite_union (i : exp) (s : exp) : exp =
  Union (i, s)

(Measure). For and disjoint , .

let measure_union (mu : exp) (s : exp) =
  SetEq (App (mu, Union (Nat, s)),
    Sum (Nat, Lam ("n", Nat,
      App (mu, App (s, Var "n")))))