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:
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)
#
@[simp]
theorem
Set.Icc.mk_zero
{α : Type u_1}
[inst : OrderedSemiring α]
(h : 0 ∈ Set.Icc 0 1)
:
{ val := 0, property := h } = 0
@[simp]
theorem
Set.Icc.mk_one
{α : Type u_1}
[inst : OrderedSemiring α]
(h : 1 ∈ Set.Icc 0 1)
:
{ val := 1, property := h } = 1
@[simp]
@[simp]
like coe_nonneg
, but with the inequality in Icc (0:α) 1
.
like coe_le_one
, but with the inequality in Icc (0:α) 1
.
@[simp]
theorem
Set.Icc.coe_mul
{α : Type u_1}
[inst : OrderedSemiring α]
(x : ↑(Set.Icc 0 1))
(y : ↑(Set.Icc 0 1))
:
@[simp]
theorem
Set.Icc.mul_le_left
{α : Type u_1}
[inst : OrderedSemiring α]
{x : ↑(Set.Icc 0 1)}
{y : ↑(Set.Icc 0 1)}
:
theorem
Set.Icc.mul_le_right
{α : Type u_1}
[inst : OrderedSemiring α]
{x : ↑(Set.Icc 0 1)}
{y : ↑(Set.Icc 0 1)}
:
instance
Set.Icc.monoidWithZero
{α : Type u_1}
[inst : OrderedSemiring α]
:
MonoidWithZero ↑(Set.Icc 0 1)
Equations
- One or more equations did not get rendered due to their size.
instance
Set.Icc.commMonoidWithZero
{α : Type u_1}
[inst : OrderedCommSemiring α]
:
CommMonoidWithZero ↑(Set.Icc 0 1)
Equations
- One or more equations did not get rendered due to their size.
instance
Set.Icc.cancelMonoidWithZero
{α : Type u_1}
[inst : OrderedRing α]
[inst : NoZeroDivisors α]
:
CancelMonoidWithZero ↑(Set.Icc 0 1)
Equations
- One or more equations did not get rendered due to their size.
instance
Set.Icc.cancelCommMonoidWithZero
{α : Type u_1}
[inst : OrderedCommRing α]
[inst : NoZeroDivisors α]
:
CancelCommMonoidWithZero ↑(Set.Icc 0 1)
Equations
- One or more equations did not get rendered due to their size.
Instances for ↥(Set.Ico 0 1)
#
@[simp]
@[simp]
theorem
Set.Ico.mk_zero
{α : Type u_1}
[inst : OrderedSemiring α]
[inst : Nontrivial α]
(h : 0 ∈ Set.Ico 0 1)
:
{ val := 0, property := h } = 0
@[simp]
theorem
Set.Ico.coe_eq_zero
{α : Type u_1}
[inst : OrderedSemiring α]
[inst : Nontrivial α]
{x : ↑(Set.Ico 0 1)}
:
theorem
Set.Ico.coe_ne_zero
{α : Type u_1}
[inst : OrderedSemiring α]
[inst : Nontrivial α]
{x : ↑(Set.Ico 0 1)}
:
theorem
Set.Ico.nonneg
{α : Type u_1}
[inst : OrderedSemiring α]
[inst : Nontrivial α]
{t : ↑(Set.Ico 0 1)}
:
0 ≤ t
like coe_nonneg
, but with the inequality in Ico (0:α) 1
.
@[simp]
theorem
Set.Ico.coe_mul
{α : Type u_1}
[inst : OrderedSemiring α]
(x : ↑(Set.Ico 0 1))
(y : ↑(Set.Ico 0 1))
:
Equations
- Set.Ico.semigroup = Function.Injective.semigroup (fun a => ↑a) (_ : Function.Injective fun a => ↑a) (_ : ∀ (x y : ↑(Set.Ico 0 1)), ↑(x * y) = ↑x * ↑y)
instance
Set.Ico.commSemigroup
{α : Type u_1}
[inst : OrderedCommSemiring α]
:
CommSemigroup ↑(Set.Ico 0 1)
Equations
- Set.Ico.commSemigroup = Function.Injective.commSemigroup (fun a => ↑a) (_ : Function.Injective fun a => ↑a) (_ : ∀ (x y : ↑(Set.Ico 0 1)), ↑(x * y) = ↑x * ↑y)
Instances for ↥(set.Ioc 0 1)
#
@[simp]
theorem
Set.Ioc.coe_one
{α : Type u_1}
[inst : StrictOrderedSemiring α]
[inst : Nontrivial α]
:
↑1 = 1
@[simp]
theorem
Set.Ioc.mk_one
{α : Type u_1}
[inst : StrictOrderedSemiring α]
[inst : Nontrivial α]
(h : 1 ∈ Set.Ioc 0 1)
:
{ val := 1, property := h } = 1
@[simp]
theorem
Set.Ioc.coe_eq_one
{α : Type u_1}
[inst : StrictOrderedSemiring α]
[inst : Nontrivial α]
{x : ↑(Set.Ioc 0 1)}
:
theorem
Set.Ioc.coe_ne_one
{α : Type u_1}
[inst : StrictOrderedSemiring α]
[inst : Nontrivial α]
{x : ↑(Set.Ioc 0 1)}
:
theorem
Set.Ioc.coe_pos
{α : Type u_1}
[inst : StrictOrderedSemiring α]
(x : ↑(Set.Ioc 0 1))
:
0 < ↑x
theorem
Set.Ioc.coe_le_one
{α : Type u_1}
[inst : StrictOrderedSemiring α]
(x : ↑(Set.Ioc 0 1))
:
↑x ≤ 1
theorem
Set.Ioc.le_one
{α : Type u_1}
[inst : StrictOrderedSemiring α]
[inst : Nontrivial α]
{t : ↑(Set.Ioc 0 1)}
:
t ≤ 1
like coe_le_one
, but with the inequality in Ioc (0:α) 1
.
@[simp]
theorem
Set.Ioc.coe_mul
{α : Type u_1}
[inst : StrictOrderedSemiring α]
(x : ↑(Set.Ioc 0 1))
(y : ↑(Set.Ioc 0 1))
:
@[simp]
theorem
Set.Ioc.coe_pow
{α : Type u_1}
[inst : StrictOrderedSemiring α]
(x : ↑(Set.Ioc 0 1))
(n : ℕ)
:
Equations
- Set.Ioc.semigroup = Function.Injective.semigroup (fun a => ↑a) (_ : Function.Injective fun a => ↑a) (_ : ∀ (x y : ↑(Set.Ioc 0 1)), ↑(x * y) = ↑x * ↑y)
Equations
- One or more equations did not get rendered due to their size.
instance
Set.Ioc.commSemigroup
{α : Type u_1}
[inst : StrictOrderedCommSemiring α]
:
CommSemigroup ↑(Set.Ioc 0 1)
Equations
- Set.Ioc.commSemigroup = Function.Injective.commSemigroup (fun a => ↑a) (_ : Function.Injective fun a => ↑a) (_ : ∀ (x y : ↑(Set.Ioc 0 1)), ↑(x * y) = ↑x * ↑y)
instance
Set.Ioc.commMonoid
{α : Type u_1}
[inst : StrictOrderedCommSemiring α]
[inst : Nontrivial α]
:
CommMonoid ↑(Set.Ioc 0 1)
Equations
- One or more equations did not get rendered due to their size.
instance
Set.Ioc.cancelMonoid
{α : Type u_1}
[inst : StrictOrderedRing α]
[inst : IsDomain α]
:
CancelMonoid ↑(Set.Ioc 0 1)
instance
Set.Ioc.cancelCommMonoid
{α : Type u_1}
[inst : StrictOrderedCommRing α]
[inst : IsDomain α]
:
CancelCommMonoid ↑(Set.Ioc 0 1)
Instances for ↥(Set.Ioo 0 1)
#
theorem
Set.Ioo.lt_one
{α : Type u_1}
[inst : StrictOrderedSemiring α]
(x : ↑(Set.Ioo 0 1))
:
↑x < 1
@[simp]
theorem
Set.Ioo.coe_mul
{α : Type u_1}
[inst : StrictOrderedSemiring α]
(x : ↑(Set.Ioo 0 1))
(y : ↑(Set.Ioo 0 1))
:
Equations
- Set.Ioo.semigroup = Function.Injective.semigroup (fun a => ↑a) (_ : Function.Injective fun a => ↑a) (_ : ∀ (x y : ↑(Set.Ioo 0 1)), ↑(x * y) = ↑x * ↑y)
instance
Set.Ioo.commSemigroup
{α : Type u_1}
[inst : StrictOrderedCommSemiring α]
:
CommSemigroup ↑(Set.Ioo 0 1)
Equations
- Set.Ioo.commSemigroup = Function.Injective.commSemigroup (fun a => ↑a) (_ : Function.Injective fun a => ↑a) (_ : ∀ (x y : ↑(Set.Ioo 0 1)), ↑(x * y) = ↑x * ↑y)