# mathlib3documentation

data.set.intervals.instances

# Algebraic instances for unit intervals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

For suitably structured underlying type α, we exhibit the structure of the unit intervals (set.Icc, set.Ioc, set.Ioc, and set.Ioo) from 0 to 1.

Note: Instances for the interval Ici 0 are dealt with in algebra/order/nonneg.lean.

## Main definitions #

The strongest typeclass provided on each interval is:

• set.Icc.cancel_comm_monoid_with_zero
• set.Ico.comm_semigroup
• set.Ioc.comm_monoid
• set.Ioo.comm_semigroup

## TODO #

• algebraic instances for intervals -1 to 1
• algebraic instances for Ici 1
• algebraic instances for (Ioo (-1) 1)ᶜ
• provide has_distrib_neg instances where applicable
• prove versions of mul_le_{left,right} for other intervals
• prove versions of the lemmas in topology/unit_interval with ℝ generalized to some arbitrary ordered semiring

### Instances for ↥(set.Icc 0 1)#

@[protected, instance]
def set.Icc.has_zero {α : Type u_1}  :
Equations
@[protected, instance]
def set.Icc.has_one {α : Type u_1}  :
Equations
@[simp, norm_cast]
theorem set.Icc.coe_zero {α : Type u_1}  :
0 = 0
@[simp, norm_cast]
theorem set.Icc.coe_one {α : Type u_1}  :
1 = 1
@[simp]
theorem set.Icc.mk_zero {α : Type u_1} (h : 0 1) :
0, h⟩ = 0
@[simp]
theorem set.Icc.mk_one {α : Type u_1} (h : 1 1) :
1, h⟩ = 1
@[simp, norm_cast]
theorem set.Icc.coe_eq_zero {α : Type u_1} {x : (set.Icc 0 1)} :
x = 0 x = 0
theorem set.Icc.coe_ne_zero {α : Type u_1} {x : (set.Icc 0 1)} :
x 0 x 0
@[simp, norm_cast]
theorem set.Icc.coe_eq_one {α : Type u_1} {x : (set.Icc 0 1)} :
x = 1 x = 1
theorem set.Icc.coe_ne_one {α : Type u_1} {x : (set.Icc 0 1)} :
x 1 x 1
theorem set.Icc.coe_nonneg {α : Type u_1} (x : (set.Icc 0 1)) :
0 x
theorem set.Icc.coe_le_one {α : Type u_1} (x : (set.Icc 0 1)) :
x 1
theorem set.Icc.nonneg {α : Type u_1} {t : (set.Icc 0 1)} :
0 t

like coe_nonneg, but with the inequality in Icc (0:α) 1.

theorem set.Icc.le_one {α : Type u_1} {t : (set.Icc 0 1)} :
t 1

like coe_le_one, but with the inequality in Icc (0:α) 1.

@[protected, instance]
def set.Icc.has_mul {α : Type u_1}  :
Equations
@[protected, instance]
def set.Icc.has_pow {α : Type u_1}  :
Equations
@[simp, norm_cast]
theorem set.Icc.coe_mul {α : Type u_1} (x y : (set.Icc 0 1)) :
(x * y) = x * y
@[simp, norm_cast]
theorem set.Icc.coe_pow {α : Type u_1} (x : (set.Icc 0 1)) (n : ) :
(x ^ n) = x ^ n
theorem set.Icc.mul_le_left {α : Type u_1} {x y : (set.Icc 0 1)} :
x * y x
theorem set.Icc.mul_le_right {α : Type u_1} {x y : (set.Icc 0 1)} :
x * y y
@[protected, instance]
Equations
@[protected, instance]
def set.Icc.comm_monoid_with_zero {α : Type u_1}  :
Equations
• set.Icc.comm_monoid_with_zero = set.Icc.comm_monoid_with_zero._proof_1 set.Icc.comm_monoid_with_zero._proof_2 set.Icc.comm_monoid_with_zero._proof_3 set.Icc.comm_monoid_with_zero._proof_4 set.Icc.comm_monoid_with_zero._proof_5
@[protected, instance]
Equations
• set.Icc.cancel_monoid_with_zero = set.Icc.cancel_monoid_with_zero._proof_1 set.Icc.cancel_monoid_with_zero._proof_2 set.Icc.cancel_monoid_with_zero._proof_3 set.Icc.cancel_monoid_with_zero._proof_4 set.Icc.cancel_monoid_with_zero._proof_5
@[protected, instance]
Equations
• set.Icc.cancel_comm_monoid_with_zero = set.Icc.cancel_comm_monoid_with_zero._proof_1 set.Icc.cancel_comm_monoid_with_zero._proof_2 set.Icc.cancel_comm_monoid_with_zero._proof_3 set.Icc.cancel_comm_monoid_with_zero._proof_4 set.Icc.cancel_comm_monoid_with_zero._proof_5
theorem set.Icc.one_sub_mem {β : Type u_2} [ordered_ring β] {t : β} (ht : t 1) :
1 - t 1
theorem set.Icc.mem_iff_one_sub_mem {β : Type u_2} [ordered_ring β] {t : β} :
t 1 1 - t 1
theorem set.Icc.one_sub_nonneg {β : Type u_2} [ordered_ring β] (x : (set.Icc 0 1)) :
0 1 - x
theorem set.Icc.one_sub_le_one {β : Type u_2} [ordered_ring β] (x : (set.Icc 0 1)) :
1 - x 1

### Instances for ↥(set.Ico 0 1)#

@[protected, instance]
def set.Ico.has_zero {α : Type u_1} [nontrivial α] :
Equations
@[simp, norm_cast]
theorem set.Ico.coe_zero {α : Type u_1} [nontrivial α] :
0 = 0
@[simp]
theorem set.Ico.mk_zero {α : Type u_1} [nontrivial α] (h : 0 1) :
0, h⟩ = 0
@[simp, norm_cast]
theorem set.Ico.coe_eq_zero {α : Type u_1} [nontrivial α] {x : (set.Ico 0 1)} :
x = 0 x = 0
theorem set.Ico.coe_ne_zero {α : Type u_1} [nontrivial α] {x : (set.Ico 0 1)} :
x 0 x 0
theorem set.Ico.coe_nonneg {α : Type u_1} (x : (set.Ico 0 1)) :
0 x
theorem set.Ico.coe_lt_one {α : Type u_1} (x : (set.Ico 0 1)) :
x < 1
theorem set.Ico.nonneg {α : Type u_1} [nontrivial α] {t : (set.Ico 0 1)} :
0 t

like coe_nonneg, but with the inequality in Ico (0:α) 1.

@[protected, instance]
def set.Ico.has_mul {α : Type u_1}  :
Equations
@[simp, norm_cast]
theorem set.Ico.coe_mul {α : Type u_1} (x y : (set.Ico 0 1)) :
(x * y) = x * y
@[protected, instance]
def set.Ico.semigroup {α : Type u_1}  :
Equations
@[protected, instance]
Equations

### Instances for ↥(set.Ioc 0 1)#

@[protected, instance]
def set.Ioc.has_one {α : Type u_1} [nontrivial α] :
Equations
@[simp, norm_cast]
theorem set.Ioc.coe_one {α : Type u_1} [nontrivial α] :
1 = 1
@[simp]
theorem set.Ioc.mk_one {α : Type u_1} [nontrivial α] (h : 1 1) :
1, h⟩ = 1
@[simp, norm_cast]
theorem set.Ioc.coe_eq_one {α : Type u_1} [nontrivial α] {x : (set.Ioc 0 1)} :
x = 1 x = 1
theorem set.Ioc.coe_ne_one {α : Type u_1} [nontrivial α] {x : (set.Ioc 0 1)} :
x 1 x 1
theorem set.Ioc.coe_pos {α : Type u_1} (x : (set.Ioc 0 1)) :
0 < x
theorem set.Ioc.coe_le_one {α : Type u_1} (x : (set.Ioc 0 1)) :
x 1
theorem set.Ioc.le_one {α : Type u_1} [nontrivial α] {t : (set.Ioc 0 1)} :
t 1

like coe_le_one, but with the inequality in Ioc (0:α) 1.

@[protected, instance]
def set.Ioc.has_mul {α : Type u_1}  :
Equations
@[protected, instance]
def set.Ioc.has_pow {α : Type u_1}  :
Equations
@[simp, norm_cast]
theorem set.Ioc.coe_mul {α : Type u_1} (x y : (set.Ioc 0 1)) :
(x * y) = x * y
@[simp, norm_cast]
theorem set.Ioc.coe_pow {α : Type u_1} (x : (set.Ioc 0 1)) (n : ) :
(x ^ n) = x ^ n
@[protected, instance]
def set.Ioc.semigroup {α : Type u_1}  :
Equations
@[protected, instance]
def set.Ioc.monoid {α : Type u_1} [nontrivial α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
• set.Ioc.comm_monoid = set.Ioc.comm_monoid._proof_1 set.Ioc.comm_monoid._proof_2 set.Ioc.comm_monoid._proof_3 set.Ioc.comm_monoid._proof_4
@[protected, instance]
Equations
@[protected, instance]
def set.Ioc.cancel_comm_monoid {α : Type u_1} [is_domain α] :
Equations

### Instances for ↥(set.Ioo 0 1)#

theorem set.Ioo.pos {α : Type u_1} (x : (set.Ioo 0 1)) :
0 < x
theorem set.Ioo.lt_one {α : Type u_1} (x : (set.Ioo 0 1)) :
x < 1
@[protected, instance]
def set.Ioo.has_mul {α : Type u_1}  :
Equations
@[simp, norm_cast]
theorem set.Ioo.coe_mul {α : Type u_1} (x y : (set.Ioo 0 1)) :
(x * y) = x * y
@[protected, instance]
def set.Ioo.semigroup {α : Type u_1}  :
Equations
@[protected, instance]
Equations
theorem set.Ioo.one_sub_mem {β : Type u_2} [ordered_ring β] {t : β} (ht : t 1) :
1 - t 1
theorem set.Ioo.mem_iff_one_sub_mem {β : Type u_2} [ordered_ring β] {t : β} :
t 1 1 - t 1
theorem set.Ioo.one_minus_pos {β : Type u_2} [ordered_ring β] (x : (set.Ioo 0 1)) :
0 < 1 - x
theorem set.Ioo.one_minus_lt_one {β : Type u_2} [ordered_ring β] (x : (set.Ioo 0 1)) :
1 - x < 1