INFINUM

-type computes the infinum of a set of real numbers, the greatest lower bound, critical for analysis alongside . It relies on the order completeness of in this system.

In Schwartz’s framework, underpins definitions of limits, integrals, and constructive bounds, complementing supremum operations.

Formation

(-Formation). The infinum is defined over a set , yielding a real number.

type exp =
  | Inf of exp  (* Inf S *)

Introduction

(-Introduction). The infinum of a set is introduced as , assuming is non-empty and bounded below.

let inf_a : exp =
  Inf (Set (Lam ("x", Real, RealIneq (Gt, Var "x", Zero))))

Elimination

(-Elimination). The infinum acts as a lower bound, provable via its defining properties.

let lower_bound (s : exp) (inf_s : exp) =
  Forall ("x", Real, RealIneq (Lte, inf_s, Var "x"))

Computation

(-Computation). The infinum is characterized as the greatest lower bound, verifiable via Z3 for specific sets.

let infer env ctx (Inf s) = check env ctx s (Set Real); Real

Uniqueness

(-Uniqueness). The infinum of a set is unique in , as any two greatest lower bounds are equal.

let equal env ctx (Inf s1) (Inf s2) =
  equal env ctx s1 s2

Theorems

(Completeness). Every non-empty set of real numbers bounded below has an infinum in , by the system’s completeness.

(Duality with Sup). For a set , , where , linking and .

let inf_sup_dual (s : exp) =
  RealOps (Neg, Sup (Set (Lam ("x", Real,
    Exists ("y", Real, And (App (s, Var "y"),
      RealIneq (Eq, Var "x",
        RealOps (Neg, Var "y", Zero))))))))