nLab locator

Contents

Contents

Definition

Given a dense linear order AA and a countable dense linear order BB such that BAB \subseteq A, a BB-indexed locator for an element cAc \in A is an element of the indexed cartesian product of the family of functions

(]a,b[(]a,c[+]c,b[)) (a,b)B×B\left(]a,b[ \to (]a,c[ + ]c,b[)\right)_{(a,b) \in B \times B}

indexed by the cartesian product set B×BB \times B

l a:B b:B]a,b[(]a,c[+]c,b[)l \in \prod_{a:B} \prod_{b:B} ]a,b[ \to (]a,c[ + ]c,b[)

where ]a,b[]a,b[, ]a,c[]a,c[, ]c,b[]c,b[ are open intervals in AA.

Properties

See also

References

  • Auke Booij, Extensional constructive real analysis via locators, (abs:1805.06781)

Last revised on June 9, 2022 at 22:39:21. See the history of this page for a list of all contributions to it.