mathlib3 documentation

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:

TODO #

Instances for ↥(set.Icc 0 1) #

@[protected, instance]
Equations
@[protected, instance]
def set.Icc.has_one {α : Type u_1} [ordered_semiring α] :
Equations
@[simp, norm_cast]
theorem set.Icc.coe_zero {α : Type u_1} [ordered_semiring α] :
0 = 0
@[simp, norm_cast]
theorem set.Icc.coe_one {α : Type u_1} [ordered_semiring α] :
1 = 1
@[simp]
theorem set.Icc.mk_zero {α : Type u_1} [ordered_semiring α] (h : 0 set.Icc 0 1) :
0, h⟩ = 0
@[simp]
theorem set.Icc.mk_one {α : Type u_1} [ordered_semiring α] (h : 1 set.Icc 0 1) :
1, h⟩ = 1
@[simp, norm_cast]
theorem set.Icc.coe_eq_zero {α : Type u_1} [ordered_semiring α] {x : (set.Icc 0 1)} :
x = 0 x = 0
theorem set.Icc.coe_ne_zero {α : Type u_1} [ordered_semiring α] {x : (set.Icc 0 1)} :
x 0 x 0
@[simp, norm_cast]
theorem set.Icc.coe_eq_one {α : Type u_1} [ordered_semiring α] {x : (set.Icc 0 1)} :
x = 1 x = 1
theorem set.Icc.coe_ne_one {α : Type u_1} [ordered_semiring α] {x : (set.Icc 0 1)} :
x 1 x 1
theorem set.Icc.coe_nonneg {α : Type u_1} [ordered_semiring α] (x : (set.Icc 0 1)) :
0 x
theorem set.Icc.coe_le_one {α : Type u_1} [ordered_semiring α] (x : (set.Icc 0 1)) :
x 1
theorem set.Icc.nonneg {α : Type u_1} [ordered_semiring α] {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} [ordered_semiring α] {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} [ordered_semiring α] :
Equations
@[protected, instance]
Equations
@[simp, norm_cast]
theorem set.Icc.coe_mul {α : Type u_1} [ordered_semiring α] (x y : (set.Icc 0 1)) :
(x * y) = x * y
@[simp, norm_cast]
theorem set.Icc.coe_pow {α : Type u_1} [ordered_semiring α] (x : (set.Icc 0 1)) (n : ) :
(x ^ n) = x ^ n
theorem set.Icc.mul_le_left {α : Type u_1} [ordered_semiring α] {x y : (set.Icc 0 1)} :
x * y x
theorem set.Icc.mul_le_right {α : Type u_1} [ordered_semiring α] {x y : (set.Icc 0 1)} :
x * y y
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem set.Icc.one_sub_mem {β : Type u_2} [ordered_ring β] {t : β} (ht : t set.Icc 0 1) :
1 - t set.Icc 0 1
theorem set.Icc.mem_iff_one_sub_mem {β : Type u_2} [ordered_ring β] {t : β} :
t set.Icc 0 1 1 - t set.Icc 0 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]
Equations
@[simp, norm_cast]
theorem set.Ico.coe_zero {α : Type u_1} [ordered_semiring α] [nontrivial α] :
0 = 0
@[simp]
theorem set.Ico.mk_zero {α : Type u_1} [ordered_semiring α] [nontrivial α] (h : 0 set.Ico 0 1) :
0, h⟩ = 0
@[simp, norm_cast]
theorem set.Ico.coe_eq_zero {α : Type u_1} [ordered_semiring α] [nontrivial α] {x : (set.Ico 0 1)} :
x = 0 x = 0
theorem set.Ico.coe_ne_zero {α : Type u_1} [ordered_semiring α] [nontrivial α] {x : (set.Ico 0 1)} :
x 0 x 0
theorem set.Ico.coe_nonneg {α : Type u_1} [ordered_semiring α] (x : (set.Ico 0 1)) :
0 x
theorem set.Ico.coe_lt_one {α : Type u_1} [ordered_semiring α] (x : (set.Ico 0 1)) :
x < 1
theorem set.Ico.nonneg {α : Type u_1} [ordered_semiring α] [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} [ordered_semiring α] :
Equations
@[simp, norm_cast]
theorem set.Ico.coe_mul {α : Type u_1} [ordered_semiring α] (x y : (set.Ico 0 1)) :
(x * y) = x * y
@[protected, instance]
Equations
@[protected, instance]
Equations

Instances for ↥(set.Ioc 0 1) #

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

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

@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp, norm_cast]
theorem set.Ioc.coe_mul {α : Type u_1} [strict_ordered_semiring α] (x y : (set.Ioc 0 1)) :
(x * y) = x * y
@[simp, norm_cast]
theorem set.Ioc.coe_pow {α : Type u_1} [strict_ordered_semiring α] (x : (set.Ioc 0 1)) (n : ) :
(x ^ n) = x ^ n
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

Instances for ↥(set.Ioo 0 1) #

theorem set.Ioo.pos {α : Type u_1} [strict_ordered_semiring α] (x : (set.Ioo 0 1)) :
0 < x
theorem set.Ioo.lt_one {α : Type u_1} [strict_ordered_semiring α] (x : (set.Ioo 0 1)) :
x < 1
@[protected, instance]
Equations
@[simp, norm_cast]
theorem set.Ioo.coe_mul {α : Type u_1} [strict_ordered_semiring α] (x y : (set.Ioo 0 1)) :
(x * y) = x * y
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem set.Ioo.one_sub_mem {β : Type u_2} [ordered_ring β] {t : β} (ht : t set.Ioo 0 1) :
1 - t set.Ioo 0 1
theorem set.Ioo.mem_iff_one_sub_mem {β : Type u_2} [ordered_ring β] {t : β} :
t set.Ioo 0 1 1 - t set.Ioo 0 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