Documentation
Mathlib
.
Topology
.
MetricSpace
.
Pseudo
.
Real
Search
Google site search
return to top
source
Imports
Init
Mathlib.Topology.MetricSpace.Pseudo.Pi
Mathlib.Algebra.Order.Group.Pointwise.Interval
Imported by
Real
.
dist_left_le_of_mem_uIcc
Real
.
dist_right_le_of_mem_uIcc
Real
.
dist_le_of_mem_uIcc
Real
.
dist_le_of_mem_Icc
Real
.
dist_le_of_mem_Icc_01
Real
.
dist_le_of_mem_pi_Icc
Lemmas about distances between points in intervals in
ℝ
.
#
source
theorem
Real
.
dist_left_le_of_mem_uIcc
{x y z :
ℝ
}
(h :
y
∈
Set.uIcc
x
z
)
:
dist
x
y
≤
dist
x
z
source
theorem
Real
.
dist_right_le_of_mem_uIcc
{x y z :
ℝ
}
(h :
y
∈
Set.uIcc
x
z
)
:
dist
y
z
≤
dist
x
z
source
theorem
Real
.
dist_le_of_mem_uIcc
{x y x' y' :
ℝ
}
(hx :
x
∈
Set.uIcc
x'
y'
)
(hy :
y
∈
Set.uIcc
x'
y'
)
:
dist
x
y
≤
dist
x'
y'
source
theorem
Real
.
dist_le_of_mem_Icc
{x y x' y' :
ℝ
}
(hx :
x
∈
Set.Icc
x'
y'
)
(hy :
y
∈
Set.Icc
x'
y'
)
:
dist
x
y
≤
y'
-
x'
source
theorem
Real
.
dist_le_of_mem_Icc_01
{x y :
ℝ
}
(hx :
x
∈
Set.Icc
0
1
)
(hy :
y
∈
Set.Icc
0
1
)
:
dist
x
y
≤
1
source
theorem
Real
.
dist_le_of_mem_pi_Icc
{ι :
Type
u_1}
[
Fintype
ι
]
{x y x' y' :
ι
→
ℝ
}
(hx :
x
∈
Set.Icc
x'
y'
)
(hy :
y
∈
Set.Icc
x'
y'
)
:
dist
x
y
≤
dist
x'
y'