The unit interval, as a topological space #
Use open unitInterval
to turn on the notation I := Set.Icc (0 : ℝ) (1 : ℝ)
.
We provide basic instances, as well as a custom tactic for discharging
0 ≤ ↑x
, 0 ≤ 1 - ↑x
, ↑x ≤ 1
, and 1 - ↑x ≤ 1
when x : I
.
The unit interval #
theorem
unitInterval.mul_mem
{x : ℝ}
{y : ℝ}
(hx : x ∈ unitInterval)
(hy : y ∈ unitInterval)
:
x * y ∈ unitInterval
theorem
unitInterval.div_mem
{x : ℝ}
{y : ℝ}
(hx : 0 ≤ x)
(hy : 0 ≤ y)
(hxy : x ≤ y)
:
x / y ∈ unitInterval
Unit interval central symmetry.
Instances For
@[simp]
like unitInterval.nonneg
, but with the inequality in I
.
like unitInterval.le_one
, but with the inequality in I
.
A tactic that solves 0 ≤ ↑x
, 0 ≤ 1 - ↑x
, ↑x ≤ 1
, and 1 - ↑x ≤ 1
for x : I
.
Instances For
theorem
affineHomeomorph_image_I
{𝕜 : Type u_1}
[LinearOrderedField 𝕜]
[TopologicalSpace 𝕜]
[TopologicalRing 𝕜]
(a : 𝕜)
(b : 𝕜)
(h : 0 < a)
:
The image of [0,1]
under the homeomorphism fun x ↦ a * x + b
is [b, a+b]
.
def
iccHomeoI
{𝕜 : Type u_1}
[LinearOrderedField 𝕜]
[TopologicalSpace 𝕜]
[TopologicalRing 𝕜]
(a : 𝕜)
(b : 𝕜)
(h : a < b)
:
The affine homeomorphism from a nontrivial interval [a,b]
to [0,1]
.
Instances For
@[simp]
theorem
iccHomeoI_apply_coe
{𝕜 : Type u_1}
[LinearOrderedField 𝕜]
[TopologicalSpace 𝕜]
[TopologicalRing 𝕜]
(a : 𝕜)
(b : 𝕜)
(h : a < b)
(x : ↑(Set.Icc a b))
:
@[simp]
theorem
iccHomeoI_symm_apply_coe
{𝕜 : Type u_1}
[LinearOrderedField 𝕜]
[TopologicalSpace 𝕜]
[TopologicalRing 𝕜]
(a : 𝕜)
(b : 𝕜)
(h : a < b)
(x : ↑(Set.Icc 0 1))
: