Theorem dnif

Description: The "distance to nearest integer" function is a function. (Contributed by Asger C. Ipsen, 4-Apr-2021)

	Ref	Expression
Hypothesis	dnif.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
Assertion	dnif	$$⊢T:ℝ⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		dnif.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
2		id	$$⊢x\in ℝ\to x\in ℝ$$
3	2	dnicld1	$$⊢x\in ℝ\to \left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\in ℝ$$
4	1 3	fmpti	$$⊢T:ℝ⟶ℝ$$