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
Mathlib/Algebra/Order/Nonneg/Basic.lean.
Main definitions #
The strongest typeclass provided on each interval is:
Set.Icc.commMonoidWithZeroSet.Icc.instIsCancelMulZeroSet.Ico.commSemigroupSet.Ioc.commMonoidSet.Ioo.commSemigroup
TODO #
- algebraic instances for intervals -1 to 1
- algebraic instances for
Ici 1 - algebraic instances for
(Ioo (-1) 1)ᶜ - provide
distribNeginstances where applicable - prove versions of
mul_le_{left,right}for other intervals - prove versions of the lemmas in
Topology/UnitIntervalwithℝgeneralized to some arbitrary ordered semiring
Instances for ↥(Set.Icc 0 1) #
@[implicit_reducible]
instance
Set.Icc.instZero
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
:
Zero ↑(Icc 0 1)
@[implicit_reducible]
instance
Set.Icc.instOne
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
:
One ↑(Icc 0 1)
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)
:
⟨0, h⟩ = 0
@[simp]
theorem
Set.Icc.mk_one
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
(h : 1 ∈ Icc 0 1)
:
⟨1, h⟩ = 1
@[simp]
theorem
Set.Icc.coe_eq_zero
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
{x : ↑(Icc 0 1)}
:
↑x = 0 ↔ x = 0
theorem
Set.Icc.coe_ne_zero
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
{x : ↑(Icc 0 1)}
:
↑x ≠ 0 ↔ x ≠ 0
@[simp]
theorem
Set.Icc.coe_eq_one
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
{x : ↑(Icc 0 1)}
:
↑x = 1 ↔ x = 1
theorem
Set.Icc.coe_ne_one
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
{x : ↑(Icc 0 1)}
:
↑x ≠ 1 ↔ x ≠ 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.
@[implicit_reducible]
instance
Set.Icc.instMul
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
:
Mul ↑(Icc 0 1)
@[implicit_reducible]
instance
Set.Icc.instPow
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
:
Pow ↑(Icc 0 1) ℕ
@[simp]
theorem
Set.Icc.coe_mul
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
(x y : ↑(Icc 0 1))
:
↑(x * y) = ↑x * ↑y
@[simp]
theorem
Set.Icc.coe_pow
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
(x : ↑(Icc 0 1))
(n : ℕ)
:
↑(x ^ n) = ↑x ^ 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)}
:
@[implicit_reducible]
instance
Set.Icc.instMonoidWithZero
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
:
MonoidWithZero ↑(Icc 0 1)
@[implicit_reducible]
instance
Set.Icc.instCommMonoidWithZero
{R : Type u_2}
[CommSemiring R]
[PartialOrder R]
[IsOrderedRing R]
:
CommMonoidWithZero ↑(Icc 0 1)
instance
Set.Icc.instIsCancelMulZero
{R : Type u_2}
[Ring R]
[PartialOrder R]
[IsOrderedRing R]
[NoZeroDivisors R]
:
IsCancelMulZero ↑(Icc 0 1)
theorem
Set.Icc.one_sub_mem
{β : Type u_2}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
{t : β}
(ht : t ∈ Icc 0 1)
:
1 - 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) #
@[implicit_reducible]
instance
Set.Ico.instZero
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
[Nontrivial R]
:
Zero ↑(Ico 0 1)
@[simp]
theorem
Set.Ico.coe_zero
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
[Nontrivial R]
:
↑0 = 0
@[simp]
theorem
Set.Ico.mk_zero
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
[Nontrivial R]
(h : 0 ∈ Ico 0 1)
:
⟨0, h⟩ = 0
@[simp]
theorem
Set.Ico.coe_eq_zero
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
[Nontrivial R]
{x : ↑(Ico 0 1)}
:
↑x = 0 ↔ x = 0
theorem
Set.Ico.coe_ne_zero
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
[Nontrivial R]
{x : ↑(Ico 0 1)}
:
↑x ≠ 0 ↔ x ≠ 0
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.
@[implicit_reducible]
instance
Set.Ico.instMul
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
:
Mul ↑(Ico 0 1)
@[simp]
theorem
Set.Ico.coe_mul
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsOrderedRing R]
(x y : ↑(Ico 0 1))
:
↑(x * y) = ↑x * ↑y
@[implicit_reducible]
@[implicit_reducible]
instance
Set.Ico.instCommSemigroup
{R : Type u_2}
[CommSemiring R]
[PartialOrder R]
[IsOrderedRing R]
:
CommSemigroup ↑(Ico 0 1)
Instances for ↥(Set.Ioc 0 1) #
@[implicit_reducible]
instance
Set.Ioc.instOne
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
:
One ↑(Ioc 0 1)
@[simp]
theorem
Set.Ioc.coe_one
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
:
↑1 = 1
@[simp]
theorem
Set.Ioc.mk_one
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
(h : 1 ∈ Ioc 0 1)
:
⟨1, h⟩ = 1
@[simp]
theorem
Set.Ioc.coe_eq_one
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
{x : ↑(Ioc 0 1)}
:
↑x = 1 ↔ x = 1
theorem
Set.Ioc.coe_ne_one
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
{x : ↑(Ioc 0 1)}
:
↑x ≠ 1 ↔ x ≠ 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.
@[implicit_reducible]
instance
Set.Ioc.instMul
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
:
Mul ↑(Ioc 0 1)
@[implicit_reducible]
instance
Set.Ioc.instPow
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
:
Pow ↑(Ioc 0 1) ℕ
@[simp]
theorem
Set.Ioc.coe_mul
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
(x y : ↑(Ioc 0 1))
:
↑(x * y) = ↑x * ↑y
@[simp]
theorem
Set.Ioc.coe_pow
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
(x : ↑(Ioc 0 1))
(n : ℕ)
:
↑(x ^ n) = ↑x ^ n
@[implicit_reducible]
instance
Set.Ioc.instSemigroup
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
:
@[implicit_reducible]
@[implicit_reducible]
instance
Set.Ioc.instCommSemigroup
{R : Type u_2}
[CommSemiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
:
CommSemigroup ↑(Ioc 0 1)
@[implicit_reducible]
instance
Set.Ioc.instCommMonoid
{R : Type u_2}
[CommSemiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
:
CommMonoid ↑(Ioc 0 1)
@[implicit_reducible]
instance
Set.Ioc.instCancelMonoid
{R : Type u_2}
[Ring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[IsDomain R]
:
CancelMonoid ↑(Ioc 0 1)
@[implicit_reducible]
instance
Set.Ioc.instCancelCommMonoid
{R : Type u_2}
[CommRing R]
[PartialOrder R]
[IsStrictOrderedRing R]
[IsDomain R]
:
CancelCommMonoid ↑(Ioc 0 1)
Instances for ↥(Set.Ioo 0 1) #
@[implicit_reducible]
instance
Set.Ioo.instMul
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
:
Mul ↑(Ioo 0 1)
@[simp]
theorem
Set.Ioo.coe_mul
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
(x y : ↑(Ioo 0 1))
:
↑(x * y) = ↑x * ↑y
@[implicit_reducible]
instance
Set.Ioo.instSemigroup
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
:
@[implicit_reducible]
instance
Set.Ioo.instCommSemigroup
{R : Type u_2}
[CommSemiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
:
CommSemigroup ↑(Ioo 0 1)
theorem
Set.Ioo.one_sub_mem
{β : Type u_2}
[Ring β]
[PartialOrder β]
[IsOrderedRing β]
{t : β}
(ht : t ∈ Ioo 0 1)
:
1 - 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))
: