Talk:Floor function

Phrasing the characteristic property

I've proved on paper that given $\text{Floor}:\mathbb{R}_{\ge 0}\rightarrow\mathbb{N}_{\ge 0}$ and property 3 on the previous page (the epsilon one) that properties 1 and 2 follow as well as a corollary - getting to the corollary is why I'm bothering with this.

Do I keep the characteristic property as is? Or do I adjust it to include the function statement? Both or do I combine them like below:

• Characteristic property:$\newcommand{\Floor}[1]{ {\text{Floor}{\left({#1}\right)} } }$
  • $$\Big(\forall x\in\mathbb{R}_{\ge 0}\big[\Floor{x}\in\mathbb{N}_{\ge 0}\subseteq\mathbb{R}_{\ge 0}\big]\Big)\wedge\Big(\forall x\in\mathbb{R}_{\ge 0}\exists\epsilon\in[0,1)\subseteq\mathbb{R}_{\ge 0}\big[\Floor{x}+\epsilon\eq x\big]\Big)$$
• So
  • $$\forall x\in\mathbb{R}_{\ge 0}\Big[\big(\Floor{x}\in\mathbb{N}_{\ge 0}\subseteq\mathbb{R}_{\ge 0}\big)\wedge\big(\exists\epsilon\in[0,1)\subseteq\mathbb{R}_{\ge 0}[\Floor{x}+\epsilon\eq x]\big)\Big]$$

Signed Alec (talk) 18:09, 16 January 2018 (UTC)