Homotopy Type Theory sigma-continuous valuation > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Contents

< sigma-continuous valuation

Whenever editing is allowed on the nLab again, this article should be ported over there.

Definition

In set theory

In measure theory, a σ\sigma-continuous valuation on a $\sigma$-complete lattice (L,,,,,,)(L, \leq, \bot, \vee, \top, \wedge, \Vee) is a valuation μ:L[0,]\mu:L \to [0, \infty] such that the σ\sigma-continuity condition is satisfied

sL .(n.s(n)s(n+1))(μ( n:s(n))sup n:μ(s(n)))\forall s \in L^\mathbb{N}. (\forall n \in\mathbb{N}. s(n) \leq s(n + 1)) \implies \left(\mu(\Vee_{n:\mathbb{N}} s(n)) \leq \sup_{n:\mathbb{N}} \mu(s(n)) \right)

In homotopy type theory

In measure theory, a σ\sigma-continuous valuation on a $\sigma$-complete lattice (L,,,,,,)(L, \leq, \bot, \vee, \top, \wedge, \Vee) is a valuation μ:L[0,]\mu:L \to [0, \infty] with

  • a family of dependent terms
    s:Lc(s):( n:s(n)s(n+1))(μ( n:s(n))sup n:μ(s(n)))s:\mathbb{N} \to L \vdash c(s):\left(\prod_{n:\mathbb{N}} s(n) \leq s(n + 1)\right) \to \left(\mu(\Vee_{n:\mathbb{N}} s(n)) \leq \sup_{n:\mathbb{N}} \mu(s(n)) \right)

    representing the σ\sigma-continuity condition.

See also

References

Revision on June 9, 2022 at 08:58:44 by Anonymous?. See the history of this page for a list of all contributions to it.