Algebraic instances for unit intervals #
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.cancelCommMonoidWithZero
Set.Ico.commSemigroup
Set.Ioc.commMonoid
Set.Ioo.commSemigroup
TODO #
- algebraic instances for intervals -1 to 1
- algebraic instances for
Ici 1
- algebraic instances for
(Ioo (-1) 1)ᶜ
- provide
distribNeg
instances where applicable - prove versions of
mul_le_{left,right}
for other intervals - prove versions of the lemmas in
Topology/UnitInterval
withℝ
generalized to some arbitrary ordered semiring
Instances for ↥(Set.Icc 0 1)
#
Equations
Equations
instance
Set.Icc.instZeroLEOneClass
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
:
ZeroLEOneClass ↑(Icc 0 1)
@[simp]
@[simp]
@[simp]
theorem
Set.Icc.mk_zero
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
(h : 0 ∈ Icc 0 1)
:
@[simp]
theorem
Set.Icc.mk_one
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
(h : 1 ∈ Icc 0 1)
:
@[simp]
theorem
Set.Icc.coe_eq_zero
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
{x : ↑(Icc 0 1)}
:
theorem
Set.Icc.coe_ne_zero
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
{x : ↑(Icc 0 1)}
:
@[simp]
theorem
Set.Icc.coe_eq_one
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
{x : ↑(Icc 0 1)}
:
theorem
Set.Icc.coe_ne_one
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
{x : ↑(Icc 0 1)}
:
theorem
Set.Icc.nonneg
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
{t : ↑(Icc 0 1)}
:
like coe_nonneg
, but with the inequality in Icc (0:R) 1
.
theorem
Set.Icc.le_one
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
{t : ↑(Icc 0 1)}
:
like coe_le_one
, but with the inequality in Icc (0:R) 1
.
Equations
Equations
@[simp]
theorem
Set.Icc.coe_mul
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
(x y : ↑(Icc 0 1))
:
@[simp]
theorem
Set.Icc.coe_pow
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
(x : ↑(Icc 0 1))
(n : ℕ)
:
theorem
Set.Icc.mul_le_left
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
{x y : ↑(Icc 0 1)}
:
theorem
Set.Icc.mul_le_right
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
{x y : ↑(Icc 0 1)}
:
instance
Set.Icc.instMonoidWithZero
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
:
MonoidWithZero ↑(Icc 0 1)
Equations
instance
Set.Icc.instCommMonoidWithZero
{R : Type u_2}
[CommSemiring R]
[PartialOrder R]
[IsOrderedRing R]
:
CommMonoidWithZero ↑(Icc 0 1)
Equations
instance
Set.Icc.instCancelMonoidWithZero
{R : Type u_2}
[Ring R]
[PartialOrder R]
[IsOrderedRing R]
[NoZeroDivisors R]
:
CancelMonoidWithZero ↑(Icc 0 1)
Equations
instance
Set.Icc.instCancelCommMonoidWithZero
{R : Type u_2}
[CommRing R]
[PartialOrder R]
[IsOrderedRing R]
[NoZeroDivisors R]
:
CancelCommMonoidWithZero ↑(Icc 0 1)
Equations
theorem
Set.Icc.one_sub_mem
{β : Type u_2}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
{t : β}
(ht : t ∈ Icc 0 1)
:
theorem
Set.Icc.mem_iff_one_sub_mem
{β : Type u_2}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
{t : β}
:
theorem
Set.Icc.one_sub_nonneg
{β : Type u_2}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
(x : ↑(Icc 0 1))
:
theorem
Set.Icc.one_sub_le_one
{β : Type u_2}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
(x : ↑(Icc 0 1))
:
Instances for ↥(Set.Ico 0 1)
#
instance
Set.Ico.instZero
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
[Nontrivial R]
:
Equations
@[simp]
theorem
Set.Ico.coe_zero
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
[Nontrivial R]
:
@[simp]
theorem
Set.Ico.mk_zero
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
[Nontrivial R]
(h : 0 ∈ Ico 0 1)
:
@[simp]
theorem
Set.Ico.coe_eq_zero
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
[Nontrivial R]
{x : ↑(Ico 0 1)}
:
theorem
Set.Ico.coe_ne_zero
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
[Nontrivial R]
{x : ↑(Ico 0 1)}
:
theorem
Set.Ico.nonneg
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
[Nontrivial R]
{t : ↑(Ico 0 1)}
:
like coe_nonneg
, but with the inequality in Ico (0:R) 1
.
Equations
@[simp]
theorem
Set.Ico.coe_mul
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
(x y : ↑(Ico 0 1))
:
Equations
instance
Set.Ico.instCommSemigroup
{R : Type u_2}
[CommSemiring R]
[PartialOrder R]
[IsOrderedRing R]
:
CommSemigroup ↑(Ico 0 1)
Equations
Instances for ↥(Set.Ioc 0 1)
#
Equations
@[simp]
@[simp]
theorem
Set.Ioc.mk_one
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
(h : 1 ∈ Ioc 0 1)
:
@[simp]
theorem
Set.Ioc.coe_eq_one
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
{x : ↑(Ioc 0 1)}
:
theorem
Set.Ioc.coe_ne_one
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
{x : ↑(Ioc 0 1)}
:
theorem
Set.Ioc.le_one
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
{t : ↑(Ioc 0 1)}
:
like coe_le_one
, but with the inequality in Ioc (0:R) 1
.
Equations
Equations
@[simp]
theorem
Set.Ioc.coe_mul
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
(x y : ↑(Ioc 0 1))
:
@[simp]
theorem
Set.Ioc.coe_pow
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
(x : ↑(Ioc 0 1))
(n : ℕ)
:
instance
Set.Ioc.instSemigroup
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
:
Equations
Equations
instance
Set.Ioc.instCommSemigroup
{R : Type u_2}
[CommSemiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
:
CommSemigroup ↑(Ioc 0 1)
Equations
instance
Set.Ioc.instCommMonoid
{R : Type u_2}
[CommSemiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
:
CommMonoid ↑(Ioc 0 1)
Equations
instance
Set.Ioc.instCancelMonoid
{R : Type u_2}
[Ring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[IsDomain R]
:
CancelMonoid ↑(Ioc 0 1)
Equations
instance
Set.Ioc.instCancelCommMonoid
{R : Type u_2}
[CommRing R]
[PartialOrder R]
[IsStrictOrderedRing R]
[IsDomain R]
:
CancelCommMonoid ↑(Ioc 0 1)
Equations
Instances for ↥(Set.Ioo 0 1)
#
Equations
@[simp]
theorem
Set.Ioo.coe_mul
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
(x y : ↑(Ioo 0 1))
:
instance
Set.Ioo.instSemigroup
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
:
Equations
instance
Set.Ioo.instCommSemigroup
{R : Type u_2}
[CommSemiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
:
CommSemigroup ↑(Ioo 0 1)
Equations
theorem
Set.Ioo.one_sub_mem
{β : Type u_2}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
{t : β}
(ht : t ∈ Ioo 0 1)
:
theorem
Set.Ioo.mem_iff_one_sub_mem
{β : Type u_2}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
{t : β}
:
theorem
Set.Ioo.one_minus_pos
{β : Type u_2}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
(x : ↑(Ioo 0 1))
:
theorem
Set.Ioo.one_minus_lt_one
{β : Type u_2}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
(x : ↑(Ioo 0 1))
: