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 #

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)` #

source

@[protected, instance]

def set.Icc.has_zero {α : Type u_1} [ordered_semiring α] :

has_zero ↥(set.Icc 0 1)

Equations

set.Icc.has_zero = {zero := ⟨0, _⟩}

source

@[protected, instance]

def set.Icc.has_one {α : Type u_1} [ordered_semiring α] :

has_one ↥(set.Icc 0 1)

Equations

set.Icc.has_one = {one := ⟨1, _⟩}

source

@[simp, norm_cast]

theorem set.Icc.coe_zero {α : Type u_1} [ordered_semiring α] :

↑0 = 0

source

@[simp, norm_cast]

theorem set.Icc.coe_one {α : Type u_1} [ordered_semiring α] :

↑1 = 1

source

@[simp]

theorem set.Icc.mk_zero {α : Type u_1} [ordered_semiring α] (h : 0 ∈ set.Icc 0 1) :

⟨0, h⟩ = 0

source

@[simp]

theorem set.Icc.mk_one {α : Type u_1} [ordered_semiring α] (h : 1 ∈ set.Icc 0 1) :

⟨1, h⟩ = 1

source

@[simp, norm_cast]

theorem set.Icc.coe_eq_zero {α : Type u_1} [ordered_semiring α] {x : ↥(set.Icc 0 1)} :

↑x = 0 ↔ x = 0

source

theorem set.Icc.coe_ne_zero {α : Type u_1} [ordered_semiring α] {x : ↥(set.Icc 0 1)} :

↑x ≠ 0 ↔ x ≠ 0

source

@[simp, norm_cast]

theorem set.Icc.coe_eq_one {α : Type u_1} [ordered_semiring α] {x : ↥(set.Icc 0 1)} :

↑x = 1 ↔ x = 1

source

theorem set.Icc.coe_ne_one {α : Type u_1} [ordered_semiring α] {x : ↥(set.Icc 0 1)} :

↑x ≠ 1 ↔ x ≠ 1

source

theorem set.Icc.coe_nonneg {α : Type u_1} [ordered_semiring α] (x : ↥(set.Icc 0 1)) :

0 ≤ ↑x

source

theorem set.Icc.coe_le_one {α : Type u_1} [ordered_semiring α] (x : ↥(set.Icc 0 1)) :

↑x ≤ 1

source

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.

source

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.

source

@[protected, instance]

def set.Icc.has_mul {α : Type u_1} [ordered_semiring α] :

has_mul ↥(set.Icc 0 1)

Equations

set.Icc.has_mul = {mul := λ (p q : ↥(set.Icc 0 1)), ⟨↑p * ↑q, _⟩}

source

@[protected, instance]

def set.Icc.has_pow {α : Type u_1} [ordered_semiring α] :

has_pow ↥(set.Icc 0 1) ℕ

Equations

set.Icc.has_pow = {pow := λ (p : ↥(set.Icc 0 1)) (n : ℕ), ⟨p.val ^ n, _⟩}

source

@[simp, norm_cast]

theorem set.Icc.coe_mul {α : Type u_1} [ordered_semiring α] (x y : ↥(set.Icc 0 1)) :

↑(x * y) = ↑x * ↑y

source

@[simp, norm_cast]

theorem set.Icc.coe_pow {α : Type u_1} [ordered_semiring α] (x : ↥(set.Icc 0 1)) (n : ℕ) :

↑(x ^ n) = ↑x ^ n

source

theorem set.Icc.mul_le_left {α : Type u_1} [ordered_semiring α] {x y : ↥(set.Icc 0 1)} :

x * y ≤ x

source

theorem set.Icc.mul_le_right {α : Type u_1} [ordered_semiring α] {x y : ↥(set.Icc 0 1)} :

x * y ≤ y

source

@[protected, instance]

def set.Icc.monoid_with_zero {α : Type u_1} [ordered_semiring α] :

monoid_with_zero ↥(set.Icc 0 1)

Equations

set.Icc.monoid_with_zero = function.injective.monoid_with_zero coe set.Icc.monoid_with_zero._proof_1 set.Icc.coe_zero set.Icc.coe_one set.Icc.coe_mul set.Icc.coe_pow

source

@[protected, instance]

def set.Icc.comm_monoid_with_zero {α : Type u_1} [ordered_comm_semiring α] :

comm_monoid_with_zero ↥(set.Icc 0 1)

Equations

set.Icc.comm_monoid_with_zero = function.injective.comm_monoid_with_zero coe 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

source

@[protected, instance]

def set.Icc.cancel_monoid_with_zero {α : Type u_1} [ordered_ring α] [no_zero_divisors α] :

cancel_monoid_with_zero ↥(set.Icc 0 1)

Equations

set.Icc.cancel_monoid_with_zero = function.injective.cancel_monoid_with_zero coe 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

source

@[protected, instance]

def set.Icc.cancel_comm_monoid_with_zero {α : Type u_1} [ordered_comm_ring α] [no_zero_divisors α] :

cancel_comm_monoid_with_zero ↥(set.Icc 0 1)

Equations

set.Icc.cancel_comm_monoid_with_zero = function.injective.cancel_comm_monoid_with_zero coe 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

source

theorem set.Icc.one_sub_mem {β : Type u_2} [ordered_ring β] {t : β} (ht : t ∈ set.Icc 0 1) :

1 - t ∈ set.Icc 0 1

source

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

source

theorem set.Icc.one_sub_nonneg {β : Type u_2} [ordered_ring β] (x : ↥(set.Icc 0 1)) :

0 ≤ 1 - ↑x

source

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)` #

source

@[protected, instance]

def set.Ico.has_zero {α : Type u_1} [ordered_semiring α] [nontrivial α] :

has_zero ↥(set.Ico 0 1)

Equations

set.Ico.has_zero = {zero := ⟨0, _⟩}

source

@[simp, norm_cast]

theorem set.Ico.coe_zero {α : Type u_1} [ordered_semiring α] [nontrivial α] :

↑0 = 0

source

@[simp]

theorem set.Ico.mk_zero {α : Type u_1} [ordered_semiring α] [nontrivial α] (h : 0 ∈ set.Ico 0 1) :

⟨0, h⟩ = 0

source

@[simp, norm_cast]

theorem set.Ico.coe_eq_zero {α : Type u_1} [ordered_semiring α] [nontrivial α] {x : ↥(set.Ico 0 1)} :

↑x = 0 ↔ x = 0

source

theorem set.Ico.coe_ne_zero {α : Type u_1} [ordered_semiring α] [nontrivial α] {x : ↥(set.Ico 0 1)} :

↑x ≠ 0 ↔ x ≠ 0

source

theorem set.Ico.coe_nonneg {α : Type u_1} [ordered_semiring α] (x : ↥(set.Ico 0 1)) :

0 ≤ ↑x

source

theorem set.Ico.coe_lt_one {α : Type u_1} [ordered_semiring α] (x : ↥(set.Ico 0 1)) :

↑x < 1

source

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.

source

@[protected, instance]

def set.Ico.has_mul {α : Type u_1} [ordered_semiring α] :

has_mul ↥(set.Ico 0 1)

Equations

set.Ico.has_mul = {mul := λ (p q : ↥(set.Ico 0 1)), ⟨↑p * ↑q, _⟩}

source

@[simp, norm_cast]

theorem set.Ico.coe_mul {α : Type u_1} [ordered_semiring α] (x y : ↥(set.Ico 0 1)) :

↑(x * y) = ↑x * ↑y

source

@[protected, instance]

def set.Ico.semigroup {α : Type u_1} [ordered_semiring α] :

semigroup ↥(set.Ico 0 1)

Equations

set.Ico.semigroup = function.injective.semigroup coe set.Ico.semigroup._proof_1 set.Ico.coe_mul

source

@[protected, instance]

def set.Ico.comm_semigroup {α : Type u_1} [ordered_comm_semiring α] :

comm_semigroup ↥(set.Ico 0 1)

Equations

set.Ico.comm_semigroup = function.injective.comm_semigroup coe set.Ico.comm_semigroup._proof_1 set.Ico.comm_semigroup._proof_2

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

source

@[protected, instance]

def set.Ioc.has_one {α : Type u_1} [strict_ordered_semiring α] [nontrivial α] :

has_one ↥(set.Ioc 0 1)

Equations

set.Ioc.has_one = {one := ⟨1, _⟩}

source

@[simp, norm_cast]

theorem set.Ioc.coe_one {α : Type u_1} [strict_ordered_semiring α] [nontrivial α] :

↑1 = 1

source

@[simp]

theorem set.Ioc.mk_one {α : Type u_1} [strict_ordered_semiring α] [nontrivial α] (h : 1 ∈ set.Ioc 0 1) :

⟨1, h⟩ = 1

source

@[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

source

theorem set.Ioc.coe_ne_one {α : Type u_1} [strict_ordered_semiring α] [nontrivial α] {x : ↥(set.Ioc 0 1)} :

↑x ≠ 1 ↔ x ≠ 1

source

theorem set.Ioc.coe_pos {α : Type u_1} [strict_ordered_semiring α] (x : ↥(set.Ioc 0 1)) :

0 < ↑x

source

theorem set.Ioc.coe_le_one {α : Type u_1} [strict_ordered_semiring α] (x : ↥(set.Ioc 0 1)) :

↑x ≤ 1

source

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.

source

@[protected, instance]

def set.Ioc.has_mul {α : Type u_1} [strict_ordered_semiring α] :

has_mul ↥(set.Ioc 0 1)

Equations

set.Ioc.has_mul = {mul := λ (p q : ↥(set.Ioc 0 1)), ⟨p.val * q.val, _⟩}

source

@[protected, instance]

def set.Ioc.has_pow {α : Type u_1} [strict_ordered_semiring α] :

has_pow ↥(set.Ioc 0 1) ℕ

Equations

set.Ioc.has_pow = {pow := λ (p : ↥(set.Ioc 0 1)) (n : ℕ), ⟨p.val ^ n, _⟩}

source

@[simp, norm_cast]

theorem set.Ioc.coe_mul {α : Type u_1} [strict_ordered_semiring α] (x y : ↥(set.Ioc 0 1)) :

↑(x * y) = ↑x * ↑y

source

@[simp, norm_cast]

theorem set.Ioc.coe_pow {α : Type u_1} [strict_ordered_semiring α] (x : ↥(set.Ioc 0 1)) (n : ℕ) :

↑(x ^ n) = ↑x ^ n

source

@[protected, instance]

def set.Ioc.semigroup {α : Type u_1} [strict_ordered_semiring α] :

semigroup ↥(set.Ioc 0 1)

Equations

set.Ioc.semigroup = function.injective.semigroup coe set.Ioc.semigroup._proof_1 set.Ioc.coe_mul

source

@[protected, instance]

def set.Ioc.monoid {α : Type u_1} [strict_ordered_semiring α] [nontrivial α] :

monoid ↥(set.Ioc 0 1)

Equations

set.Ioc.monoid = function.injective.monoid coe set.Ioc.monoid._proof_1 set.Ioc.coe_one set.Ioc.coe_mul set.Ioc.coe_pow

source

@[protected, instance]

def set.Ioc.comm_semigroup {α : Type u_1} [strict_ordered_comm_semiring α] :

comm_semigroup ↥(set.Ioc 0 1)

Equations

set.Ioc.comm_semigroup = function.injective.comm_semigroup coe set.Ioc.comm_semigroup._proof_1 set.Ioc.comm_semigroup._proof_2

source

@[protected, instance]

def set.Ioc.comm_monoid {α : Type u_1} [strict_ordered_comm_semiring α] [nontrivial α] :

comm_monoid ↥(set.Ioc 0 1)

Equations

set.Ioc.comm_monoid = function.injective.comm_monoid coe set.Ioc.comm_monoid._proof_1 set.Ioc.comm_monoid._proof_2 set.Ioc.comm_monoid._proof_3 set.Ioc.comm_monoid._proof_4

source

@[protected, instance]