Mathlib.Algebra.Order.Interval.Set.Instances

Set.Icc.zero instance

: Zero (Icc (0 : R) 1)

Full source

instance zero : Zero (Icc (0 : R) 1) where zero := ⟨0, left_mem_Icc.2 zero_le_one⟩

The Zero Element in the Unit Interval

Informal description

The closed interval $[0, 1]$ in an ordered semiring $R$ has a canonical zero element, which is the element $0 \in R$ restricted to the interval.

Set.Icc.one instance

: One (Icc (0 : R) 1)

Full source

instance one : One (Icc (0 : R) 1) where one := ⟨1, right_mem_Icc.2 zero_le_one⟩

The One Element in the Unit Interval

Informal description

The closed interval $[0, 1]$ in an ordered semiring $R$ has a canonical one element, which is the element $1 \in R$ restricted to the interval.

Set.Icc.coe_zero theorem

: ↑(0 : Icc (0 : R) 1) = (0 : R)

Full source

@[simp, norm_cast]
theorem coe_zero : ↑(0 : Icc (0 : R) 1) = (0 : R) :=
  rfl

Embedding of Zero in Unit Interval Equals Zero in Semiring

Informal description

The canonical embedding of the zero element in the closed unit interval $[0,1]$ of an ordered semiring $R$ is equal to the zero element of $R$, i.e., $\uparrow(0 : [0,1]) = (0 : R)$.

Set.Icc.coe_one theorem

: ↑(1 : Icc (0 : R) 1) = (1 : R)

Full source

@[simp, norm_cast]
theorem coe_one : ↑(1 : Icc (0 : R) 1) = (1 : R) :=
  rfl

Embedding of One in Unit Interval Equals One in Semiring

Informal description

The canonical embedding of the element $1$ in the closed unit interval $[0, 1]$ of an ordered semiring $R$ is equal to the element $1$ in $R$.

Set.Icc.mk_zero theorem

(h : (0 : R) ∈ Icc (0 : R) 1) : (⟨0, h⟩ : Icc (0 : R) 1) = 0

Full source

@[simp]
theorem mk_zero (h : (0 : R) ∈ Icc (0 : R) 1) : (⟨0, h⟩ : Icc (0 : R) 1) = 0 :=
  rfl

Zero Element Construction in Unit Interval

Informal description

For any ordered semiring $R$, if $0 \in [0,1]$, then the element $\langle 0, h \rangle$ in the closed interval $[0,1]$ is equal to the zero element of the interval.

Set.Icc.mk_one theorem

(h : (1 : R) ∈ Icc (0 : R) 1) : (⟨1, h⟩ : Icc (0 : R) 1) = 1

Full source

@[simp]
theorem mk_one (h : (1 : R) ∈ Icc (0 : R) 1) : (⟨1, h⟩ : Icc (0 : R) 1) = 1 :=
  rfl

Canonical One Element in Unit Interval

Informal description

For any ordered semiring $R$, if $1$ is an element of the closed interval $[0, 1]$, then the element $\langle 1, h \rangle$ in the subtype $[0, 1]$ is equal to the canonical one element of $[0, 1]$.

Set.Icc.coe_eq_zero theorem

{x : Icc (0 : R) 1} : (x : R) = 0 ↔ x = 0

Full source

@[simp, norm_cast]
theorem coe_eq_zero {x : Icc (0 : R) 1} : (x : R) = 0 ↔ x = 0 := by
  symm
  exact Subtype.ext_iff

Characterization of Zero in the Unit Interval: $x = 0 \leftrightarrow x = 0$ in $[0,1]$

Informal description

For any element $x$ in the closed unit interval $[0, 1]$ of an ordered semiring $R$, the underlying value of $x$ in $R$ is equal to $0$ if and only if $x$ is the zero element of the interval.

Set.Icc.coe_ne_zero theorem

{x : Icc (0 : R) 1} : (x : R) ≠ 0 ↔ x ≠ 0

Full source

theorem coe_ne_zero {x : Icc (0 : R) 1} : (x : R) ≠ 0(x : R) ≠ 0 ↔ x ≠ 0 :=
  not_iff_not.mpr coe_eq_zero

Nonzero Characterization in Unit Interval: $(x : R) \neq 0 \leftrightarrow x \neq 0$ for $x \in [0,1]$

Informal description

For any element $x$ in the closed unit interval $[0, 1]$ of an ordered semiring $R$, the underlying value of $x$ in $R$ is not equal to $0$ if and only if $x$ is not the zero element of the interval.

Set.Icc.coe_eq_one theorem

{x : Icc (0 : R) 1} : (x : R) = 1 ↔ x = 1

Full source

@[simp, norm_cast]
theorem coe_eq_one {x : Icc (0 : R) 1} : (x : R) = 1 ↔ x = 1 := by
  symm
  exact Subtype.ext_iff

Characterization of One in Unit Interval: $(x : R) = 1 \leftrightarrow x = 1$ for $x \in [0,1]$

Informal description

For any element $x$ in the closed interval $[0,1]$ of an ordered semiring $R$, the underlying value of $x$ in $R$ equals $1$ if and only if $x$ is equal to the canonical one element of the interval.

Set.Icc.coe_ne_one theorem

{x : Icc (0 : R) 1} : (x : R) ≠ 1 ↔ x ≠ 1

Full source

theorem coe_ne_one {x : Icc (0 : R) 1} : (x : R) ≠ 1(x : R) ≠ 1 ↔ x ≠ 1 :=
  not_iff_not.mpr coe_eq_one

Characterization of Non-One Elements in Unit Interval: $(x : R) \neq 1 \leftrightarrow x \neq 1$ for $x \in [0,1]$

Informal description

For any element $x$ in the closed interval $[0,1]$ of an ordered semiring $R$, the underlying value of $x$ in $R$ is not equal to $1$ if and only if $x$ is not equal to the canonical one element of the interval.

Set.Icc.coe_nonneg theorem

(x : Icc (0 : R) 1) : 0 ≤ (x : R)

Full source

theorem coe_nonneg (x : Icc (0 : R) 1) : 0 ≤ (x : R) :=
  x.2.1

Nonnegativity of Elements in Unit Interval $[0,1]$

Informal description

For any element $x$ in the closed interval $[0,1]$ of a partially ordered type $R$, the underlying value of $x$ (when viewed as an element of $R$) is nonnegative, i.e., $0 \leq x$.

Set.Icc.coe_le_one theorem

(x : Icc (0 : R) 1) : (x : R) ≤ 1

Full source

theorem coe_le_one (x : Icc (0 : R) 1) : (x : R) ≤ 1 :=
  x.2.2

Upper Bound for Elements in Unit Interval $[0, 1]$

Informal description

For any element $x$ in the closed interval $[0, 1]$ of a type $R$ with a partial order, the underlying value of $x$ (when viewed as an element of $R$) is less than or equal to $1$, i.e., $x \leq 1$.

Set.Icc.nonneg theorem

{t : Icc (0 : R) 1} : 0 ≤ t

Full source

/-- like `coe_nonneg`, but with the inequality in `Icc (0:R) 1`. -/
theorem nonneg {t : Icc (0 : R) 1} : 0 ≤ t :=
  t.2.1

Nonnegativity of Elements in the Unit Interval $[0,1]$

Informal description

For any element $t$ in the closed interval $[0, 1]$ of an ordered semiring $R$, we have $0 \leq t$.

Set.Icc.le_one theorem

{t : Icc (0 : R) 1} : t ≤ 1

Full source

/-- like `coe_le_one`, but with the inequality in `Icc (0:R) 1`. -/
theorem le_one {t : Icc (0 : R) 1} : t ≤ 1 :=
  t.2.2

Upper bound property of the unit interval $[0, 1]$

Informal description

For any element $t$ in the closed interval $[0, 1]$ of an ordered semiring $R$, we have $t \leq 1$.

Set.Icc.mul instance

: Mul (Icc (0 : R) 1)

Full source

instance mul : Mul (Icc (0 : R) 1) where
  mul p q := ⟨p * q, ⟨mul_nonneg p.2.1 q.2.1, mul_le_one₀ p.2.2 q.2.1 q.2.2⟩⟩

Multiplication Operation on the Unit Interval $[0, 1]$

Informal description

For any ordered semiring $R$, the closed interval $[0, 1]$ in $R$ is equipped with a multiplication operation, where for any $x, y \in [0, 1]$, the product $x \cdot y$ is defined as the multiplication of $x$ and $y$ in $R$.

Set.Icc.pow instance

: Pow (Icc (0 : R) 1) ℕ

Full source

instance pow : Pow (Icc (0 : R) 1) ℕ where
  pow p n := ⟨p.1 ^ n, ⟨pow_nonneg p.2.1 n, pow_le_one₀ p.2.1 p.2.2⟩⟩

Natural Power Operation on the Unit Interval $[0, 1]$

Informal description

For any ordered semiring $R$, the closed interval $[0, 1]$ in $R$ is equipped with a natural power operation, where for any $x \in [0, 1]$ and natural number $n$, the power $x^n$ is defined as the $n$-fold multiplication of $x$ in $R$.

Set.Icc.coe_mul theorem

(x y : Icc (0 : R) 1) : ↑(x * y) = (x * y : R)

Full source

@[simp, norm_cast]
theorem coe_mul (x y : Icc (0 : R) 1) : ↑(x * y) = (x * y : R) :=
  rfl

Embedding Preserves Multiplication in Unit Interval $[0, 1]$

Informal description

For any elements $x, y$ in the closed interval $[0, 1]$ of an ordered semiring $R$, the canonical embedding of their product in $R$ equals the product of their embeddings, i.e., $(x \cdot y) = (x : R) \cdot (y : R)$.

Set.Icc.coe_pow theorem

(x : Icc (0 : R) 1) (n : ℕ) : ↑(x ^ n) = ((x : R) ^ n)

Full source

@[simp, norm_cast]
theorem coe_pow (x : Icc (0 : R) 1) (n : ℕ) : ↑(x ^ n) = ((x : R) ^ n) :=
  rfl

Power Operation Commutes with Inclusion on Unit Interval

Informal description

For any element $x$ in the closed interval $[0, 1]$ of an ordered semiring $R$ and any natural number $n$, the canonical inclusion map $\uparrow$ from $[0, 1]$ to $R$ satisfies $\uparrow(x^n) = (\uparrow x)^n$.

Set.Icc.mul_le_left theorem

{x y : Icc (0 : R) 1} : x * y ≤ x

Full source

theorem mul_le_left {x y : Icc (0 : R) 1} : x * y ≤ x :=
  (mul_le_mul_of_nonneg_left y.2.2 x.2.1).trans_eq (mul_one _)

Left Multiplication Inequality in Unit Interval: $x \cdot y \leq x$ for $x, y \in [0,1]$

Informal description

For any elements $x, y$ in the closed unit interval $[0, 1]$ of an ordered semiring $R$, the product $x \cdot y$ is less than or equal to $x$.

Set.Icc.mul_le_right theorem

{x y : Icc (0 : R) 1} : x * y ≤ y

Full source

theorem mul_le_right {x y : Icc (0 : R) 1} : x * y ≤ y :=
  (mul_le_mul_of_nonneg_right x.2.2 y.2.1).trans_eq (one_mul _)

Right Multiplication Inequality in Unit Interval: $x \cdot y \leq y$ for $x, y \in [0,1]$

Informal description

For any elements $x, y$ in the closed interval $[0, 1]$ of an ordered semiring $R$, the product $x \cdot y$ is less than or equal to $y$.

Set.Icc.monoidWithZero instance

: MonoidWithZero (Icc (0 : R) 1)

Full source

instance monoidWithZero : MonoidWithZero (Icc (0 : R) 1) := fast_instance%
  Subtype.coe_injective.monoidWithZero _ coe_zero coe_one coe_mul coe_pow

Monoid with Zero Structure on the Unit Interval $[0, 1]$

Informal description

For any ordered semiring $R$, the closed unit interval $[0, 1]$ in $R$ forms a monoid with zero. This means it has an associative multiplication operation with an identity element $1$ and a zero element $0$, where $0$ acts as an absorbing element (i.e., $0 \cdot x = x \cdot 0 = 0$ for all $x \in [0, 1]$).

Set.Icc.commMonoidWithZero instance

{R : Type*} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] : CommMonoidWithZero (Icc (0 : R) 1)

Full source

instance commMonoidWithZero {R : Type*} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] :
    CommMonoidWithZero (Icc (0 : R) 1) := fast_instance%
  Subtype.coe_injective.commMonoidWithZero _ coe_zero coe_one coe_mul coe_pow

Commutative Monoid with Zero Structure on the Unit Interval $[0, 1]$

Informal description

For any commutative semiring $R$ with a partial order and the structure of an ordered ring, the closed unit interval $[0, 1]$ in $R$ forms a commutative monoid with zero. This means it has an associative and commutative multiplication operation with an identity element $1$ and a zero element $0$, where $0$ acts as an absorbing element (i.e., $0 \cdot x = x \cdot 0 = 0$ for all $x \in [0, 1]$).

Set.Icc.cancelMonoidWithZero instance

{R : Type*} [Ring R] [PartialOrder R] [IsOrderedRing R] [NoZeroDivisors R] : CancelMonoidWithZero (Icc (0 : R) 1)

Full source

instance cancelMonoidWithZero {R : Type*} [Ring R] [PartialOrder R] [IsOrderedRing R]
    [NoZeroDivisors R] :
    CancelMonoidWithZero (Icc (0 : R) 1) := fast_instance%
  @Function.Injective.cancelMonoidWithZero R _ NoZeroDivisors.toCancelMonoidWithZero _ _ _ _
    (fun v => v.val) Subtype.coe_injective coe_zero coe_one coe_mul coe_pow

Cancelative Monoid with Zero Structure on the Unit Interval $[0, 1]$

Informal description

For any ordered ring $R$ with no zero divisors, the closed unit interval $[0, 1]$ forms a cancelative monoid with zero. This means it has an associative and commutative multiplication operation with an identity element $1$ and a zero element $0$, where $0$ acts as an absorbing element, and the cancellation property holds: if $x \cdot y = x \cdot z$ and $x \neq 0$, then $y = z$ for all $x, y, z \in [0, 1]$.

Set.Icc.cancelCommMonoidWithZero instance

 {R : Type*} [CommRing R] [PartialOrder R] [IsOrderedRing R] [NoZeroDivisors R] :
  CancelCommMonoidWithZero (Icc (0 : R) 1)

Full source

instance cancelCommMonoidWithZero {R : Type*} [CommRing R] [PartialOrder R] [IsOrderedRing R]
    [NoZeroDivisors R] :
    CancelCommMonoidWithZero (Icc (0 : R) 1) := fast_instance%
  @Function.Injective.cancelCommMonoidWithZero R _ NoZeroDivisors.toCancelCommMonoidWithZero _ _ _ _
    (fun v => v.val) Subtype.coe_injective coe_zero coe_one coe_mul coe_pow

Cancelative Commutative Monoid with Zero Structure on $[0,1]$

Informal description

For any commutative ordered ring $R$ with no zero divisors, the closed unit interval $[0, 1]$ forms a cancelative commutative monoid with zero. This means it has an associative and commutative multiplication operation with an identity element $1$ and a zero element $0$, where $0$ acts as an absorbing element, and the cancellation property holds: if $x \cdot y = x \cdot z$ and $x \neq 0$, then $y = z$ for all $x, y, z \in [0, 1]$.

Set.Icc.one_sub_mem theorem

{t : β} (ht : t ∈ Icc (0 : β) 1) : 1 - t ∈ Icc (0 : β) 1

Full source

theorem one_sub_mem {t : β} (ht : t ∈ Icc (0 : β) 1) : 1 - t ∈ Icc (0 : β) 1 := by
  rw [mem_Icc] at *
  exact ⟨sub_nonneg.2 ht.2, (sub_le_self_iff _).2 ht.1⟩

Closure of $1 - t$ in the Unit Interval for $t \in [0,1]$

Informal description

For any element $t$ in the closed interval $[0, 1]$ of an ordered ring $\beta$, the element $1 - t$ also belongs to the interval $[0, 1]$.

Set.Icc.mem_iff_one_sub_mem theorem

{t : β} : t ∈ Icc (0 : β) 1 ↔ 1 - t ∈ Icc (0 : β) 1

Full source

theorem mem_iff_one_sub_mem {t : β} : t ∈ Icc (0 : β) 1t ∈ Icc (0 : β) 1 ↔ 1 - t ∈ Icc (0 : β) 1 :=
  ⟨one_sub_mem, fun h => sub_sub_cancel 1 t ▸ one_sub_mem h⟩

Characterization of Unit Interval Membership via $1 - t$

Informal description

For any element $t$ in an ordered semiring $\beta$, $t$ belongs to the closed interval $[0,1]$ if and only if $1 - t$ belongs to $[0,1]$. In other words, $t \in [0,1] \leftrightarrow 1 - t \in [0,1]$.

Set.Icc.one_sub_nonneg theorem

(x : Icc (0 : β) 1) : 0 ≤ 1 - (x : β)

Full source

theorem one_sub_nonneg (x : Icc (0 : β) 1) : 0 ≤ 1 - (x : β) := by simpa using x.2.2

Nonnegativity of $1 - x$ in the unit interval

Informal description

For any element $x$ in the closed interval $[0, 1]$ of an ordered semiring $\beta$, the difference $1 - x$ is nonnegative, i.e., $0 \leq 1 - x$.

Set.Icc.one_sub_le_one theorem

(x : Icc (0 : β) 1) : 1 - (x : β) ≤ 1

Full source

theorem one_sub_le_one (x : Icc (0 : β) 1) : 1 - (x : β) ≤ 1 := by simpa using x.2.1

Upper bound for $1 - x$ in the unit interval

Informal description

For any element $x$ in the closed interval $[0, 1]$ of an ordered semiring $\beta$, the difference $1 - x$ is less than or equal to $1$.

Set.Ico.zero instance

[Nontrivial R] : Zero (Ico (0 : R) 1)

Full source

instance zero [Nontrivial R] : Zero (Ico (0 : R) 1) where zero := ⟨0, left_mem_Ico.2 zero_lt_one⟩

Zero Element in the Interval [0,1)

Informal description

For any nontrivial ordered semiring $R$, the left-closed right-open interval $[0, 1)$ has a zero element.

Set.Ico.coe_zero theorem

[Nontrivial R] : ↑(0 : Ico (0 : R) 1) = (0 : R)

Full source

@[simp, norm_cast]
theorem coe_zero [Nontrivial R] : ↑(0 : Ico (0 : R) 1) = (0 : R) :=
  rfl

Embedding of Zero in $[0,1)$ Matches Zero in $R$

Informal description

For any nontrivial ordered semiring $R$, the canonical embedding of the zero element in the interval $[0, 1)$ into $R$ is equal to the zero element of $R$. That is, if $0_{[0,1)}$ denotes the zero element of $[0, 1)$, then $0_{[0,1)} = 0_R$ under the embedding.

Set.Ico.mk_zero theorem

[Nontrivial R] (h : (0 : R) ∈ Ico (0 : R) 1) : (⟨0, h⟩ : Ico (0 : R) 1) = 0

Full source

@[simp]
theorem mk_zero [Nontrivial R] (h : (0 : R) ∈ Ico (0 : R) 1) : (⟨0, h⟩ : Ico (0 : R) 1) = 0 :=
  rfl

Zero Construction in Interval $[0,1)$

Informal description

For any nontrivial ordered semiring $R$, if $0$ is an element of the interval $[0,1)$, then the element $\langle 0, h \rangle$ in the interval $[0,1)$ is equal to the zero element of the interval.

Set.Ico.coe_eq_zero theorem

[Nontrivial R] {x : Ico (0 : R) 1} : (x : R) = 0 ↔ x = 0

Full source

@[simp, norm_cast]
theorem coe_eq_zero [Nontrivial R] {x : Ico (0 : R) 1} : (x : R) = 0 ↔ x = 0 := by
  symm
  exact Subtype.ext_iff

Characterization of Zero in the Interval [0,1)

Informal description

Let $R$ be a nontrivial ordered semiring. For any element $x$ in the interval $[0, 1) \subseteq R$, the equality $x = 0$ holds in $R$ if and only if $x$ is equal to the zero element of the interval $[0, 1)$.

Set.Ico.coe_ne_zero theorem

[Nontrivial R] {x : Ico (0 : R) 1} : (x : R) ≠ 0 ↔ x ≠ 0

Full source

theorem coe_ne_zero [Nontrivial R] {x : Ico (0 : R) 1} : (x : R) ≠ 0(x : R) ≠ 0 ↔ x ≠ 0 :=
  not_iff_not.mpr coe_eq_zero

Nonzero Characterization in $[0,1)$: $x \neq 0 \leftrightarrow x \neq 0$

Informal description

Let $R$ be a nontrivial ordered semiring. For any element $x$ in the interval $[0, 1) \subseteq R$, the inequality $x \neq 0$ holds in $R$ if and only if $x$ is not equal to the zero element of the interval $[0, 1)$.

Set.Ico.coe_nonneg theorem

(x : Ico (0 : R) 1) : 0 ≤ (x : R)

Full source

theorem coe_nonneg (x : Ico (0 : R) 1) : 0 ≤ (x : R) :=
  x.2.1

Nonnegativity of Elements in $[0, 1)$ Interval

Informal description

For any element $x$ in the left-closed right-open interval $[0, 1)$ of a type $R$ with a partial order, the value of $x$ (when viewed as an element of $R$) is nonnegative, i.e., $0 \leq x$.

Set.Ico.coe_lt_one theorem

(x : Ico (0 : R) 1) : (x : R) < 1

Full source

theorem coe_lt_one (x : Ico (0 : R) 1) : (x : R) < 1 :=
  x.2.2

Elements of $[0,1)$ are strictly less than 1

Informal description

For any element $x$ in the left-closed right-open interval $[0,1)$ of a type $R$ with a partial order, the value of $x$ (when viewed as an element of $R$) is strictly less than 1, i.e., $x < 1$.

Set.Ico.nonneg theorem

[Nontrivial R] {t : Ico (0 : R) 1} : 0 ≤ t

Full source

/-- like `coe_nonneg`, but with the inequality in `Ico (0:R) 1`. -/
theorem nonneg [Nontrivial R] {t : Ico (0 : R) 1} : 0 ≤ t :=
  t.2.1

Nonnegativity of Elements in $[0,1)$ Interval

Informal description

For any nontrivial ordered semiring $R$ and any element $t$ in the left-closed right-open interval $[0,1)$, the element $t$ is nonnegative, i.e., $0 \leq t$.

Set.Ico.mul instance

: Mul (Ico (0 : R) 1)

Full source

instance mul : Mul (Ico (0 : R) 1) where
  mul p q :=
    ⟨p * q, ⟨mul_nonneg p.2.1 q.2.1, mul_lt_one_of_nonneg_of_lt_one_right p.2.2.le q.2.1 q.2.2⟩⟩

Multiplication on the Interval $[0,1)$

Informal description

The left-closed right-open interval $[0,1)$ in an ordered semiring $R$ is equipped with a multiplication operation inherited from $R$.

Set.Ico.coe_mul theorem

(x y : Ico (0 : R) 1) : ↑(x * y) = (x * y : R)

Full source

@[simp, norm_cast]
theorem coe_mul (x y : Ico (0 : R) 1) : ↑(x * y) = (x * y : R) :=
  rfl

Embedding of Multiplication in $[0,1)$ Interval

Informal description

For any elements $x$ and $y$ in the left-closed right-open interval $[0,1)$ of an ordered semiring $R$, the canonical embedding of their product in $R$ equals the product of their embeddings, i.e., $\uparrow(x \cdot y) = (x \cdot y : R)$.

Set.Ico.semigroup instance

: Semigroup (Ico (0 : R) 1)

Full source

instance semigroup : Semigroup (Ico (0 : R) 1) := fast_instance%
  Subtype.coe_injective.semigroup _ coe_mul

Semigroup Structure on the Interval $[0,1)$

Informal description

For any ordered semiring $R$, the left-closed right-open interval $[0,1)$ forms a semigroup under the multiplication operation inherited from $R$.

Set.Ico.commSemigroup instance

{R : Type*} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] : CommSemigroup (Ico (0 : R) 1)

Full source

instance commSemigroup {R : Type*} [CommSemiring R] [PartialOrder R] [IsOrderedRing R] :
    CommSemigroup (Ico (0 : R) 1) := fast_instance%
  Subtype.coe_injective.commSemigroup _ coe_mul

Commutative Semigroup Structure on $[0,1)$ in Ordered Commutative Semirings

Informal description

For any commutative semiring $R$ with a partial order and the structure of an ordered ring, the left-closed right-open interval $[0,1)$ forms a commutative semigroup under the multiplication operation inherited from $R$.

Set.Ioc.one instance

: One (Ioc (0 : R) 1)

Full source

instance one : One (Ioc (0 : R) 1) where one := ⟨1, ⟨zero_lt_one, le_refl 1⟩⟩

Multiplicative Identity in the Interval (0, 1]

Informal description

For any strictly ordered semiring $R$, the left-open right-closed interval $(0, 1]$ in $R$ has a canonical multiplicative identity element.

Set.Ioc.coe_one theorem

: ↑(1 : Ioc (0 : R) 1) = (1 : R)

Full source

@[simp, norm_cast]
theorem coe_one : ↑(1 : Ioc (0 : R) 1) = (1 : R) :=
  rfl

Inclusion of the Identity in $(0, 1]$ Maps to $1$ in $R$

Informal description

The canonical inclusion map from the multiplicative identity element in the interval $(0, 1]$ of a strictly ordered semiring $R$ to $R$ itself maps the identity element to the multiplicative identity $1$ in $R$. In other words, if $1$ is considered as an element of $(0, 1]$, then its image under the inclusion map is $1 \in R$.

Set.Ioc.mk_one theorem

(h : (1 : R) ∈ Ioc (0 : R) 1) : (⟨1, h⟩ : Ioc (0 : R) 1) = 1

Full source

@[simp]
theorem mk_one (h : (1 : R) ∈ Ioc (0 : R) 1) : (⟨1, h⟩ : Ioc (0 : R) 1) = 1 :=
  rfl

Construction of Multiplicative Identity in Interval (0, 1]

Informal description

For any strictly ordered semiring $R$, if $1$ is an element of the interval $(0, 1]$, then the element $\langle 1, h \rangle$ of the interval $(0, 1]$ is equal to the multiplicative identity $1$ in $(0, 1]$.

Set.Ioc.coe_eq_one theorem

{x : Ioc (0 : R) 1} : (x : R) = 1 ↔ x = 1

Full source

@[simp, norm_cast]
theorem coe_eq_one {x : Ioc (0 : R) 1} : (x : R) = 1 ↔ x = 1 := by
  symm
  exact Subtype.ext_iff

Characterization of the Multiplicative Identity in $(0,1]$ Interval

Informal description

For any element $x$ in the left-open right-closed interval $(0, 1]$ of a strictly ordered semiring $R$, the underlying value of $x$ in $R$ equals $1$ if and only if $x$ is the multiplicative identity element of the interval.

Set.Ioc.coe_ne_one theorem

{x : Ioc (0 : R) 1} : (x : R) ≠ 1 ↔ x ≠ 1

Full source

theorem coe_ne_one {x : Ioc (0 : R) 1} : (x : R) ≠ 1(x : R) ≠ 1 ↔ x ≠ 1 :=
  not_iff_not.mpr coe_eq_one

Negation of Multiplicative Identity in $(0,1]$ Interval: $(x : R) \neq 1 \leftrightarrow x \neq 1$

Informal description

For any element $x$ in the left-open right-closed interval $(0, 1]$ of a strictly ordered semiring $R$, the underlying value of $x$ in $R$ is not equal to $1$ if and only if $x$ is not the multiplicative identity element of the interval.

Set.Ioc.coe_pos theorem

(x : Ioc (0 : R) 1) : 0 < (x : R)

Full source

theorem coe_pos (x : Ioc (0 : R) 1) : 0 < (x : R) :=
  x.2.1

Positivity of Elements in $(0,1]$ Interval

Informal description

For any element $x$ in the left-open right-closed interval $(0, 1]$ of a partially ordered type $R$, the underlying value of $x$ in $R$ satisfies $0 < (x : R)$.

Set.Ioc.coe_le_one theorem

(x : Ioc (0 : R) 1) : (x : R) ≤ 1

Full source

theorem coe_le_one (x : Ioc (0 : R) 1) : (x : R) ≤ 1 :=
  x.2.2

Elements of $(0,1]$ are bounded above by 1

Informal description

For any element $x$ in the left-open right-closed interval $(0, 1]$ of a type $R$ with a partial order, the underlying value of $x$ in $R$ satisfies $(x : R) \leq 1$.

Set.Ioc.le_one theorem

{t : Ioc (0 : R) 1} : t ≤ 1

Full source

/-- like `coe_le_one`, but with the inequality in `Ioc (0:R) 1`. -/
theorem le_one {t : Ioc (0 : R) 1} : t ≤ 1 :=
  t.2.2

Upper Bound of Elements in $(0,1]$ Interval

Informal description

For any element $t$ in the left-open right-closed interval $(0, 1]$ of a strictly ordered semiring $R$, we have $t \leq 1$.

Set.Ioc.mul instance

: Mul (Ioc (0 : R) 1)

Full source

instance mul : Mul (Ioc (0 : R) 1) where
  mul p q := ⟨p.1 * q.1, ⟨mul_pos p.2.1 q.2.1, mul_le_one₀ p.2.2 (le_of_lt q.2.1) q.2.2⟩⟩

Multiplication on the Interval (0, 1] in Ordered Semirings

Informal description

For any strict ordered semiring $R$, the left-open right-closed interval $(0, 1]$ is equipped with a multiplication operation inherited from $R$.

Set.Ioc.pow instance

: Pow (Ioc (0 : R) 1) ℕ

Full source

instance pow : Pow (Ioc (0 : R) 1) ℕ where
  pow p n := ⟨p.1 ^ n, ⟨pow_pos p.2.1 n, pow_le_one₀ (le_of_lt p.2.1) p.2.2⟩⟩

Natural Power Operation on the Interval (0, 1] in Ordered Semirings

Informal description

For any strict ordered semiring $R$, the left-open right-closed interval $(0, 1]$ is equipped with a natural power operation, where for any $x \in (0, 1]$ and natural number $n$, the power $x^n$ is defined as the $n$-fold multiplication of $x$ in $R$.

Set.Ioc.coe_mul theorem

(x y : Ioc (0 : R) 1) : ↑(x * y) = (x * y : R)

Full source

@[simp, norm_cast]
theorem coe_mul (x y : Ioc (0 : R) 1) : ↑(x * y) = (x * y : R) :=
  rfl

Embedding Preserves Multiplication in $(0, 1]$ Interval

Informal description

For any elements $x$ and $y$ in the left-open right-closed interval $(0, 1]$ of a strict ordered semiring $R$, the canonical embedding of their product in $R$ equals the product of their embeddings, i.e., $\uparrow(x * y) = (\uparrow x) * (\uparrow y)$ in $R$.

Set.Ioc.coe_pow theorem

(x : Ioc (0 : R) 1) (n : ℕ) : ↑(x ^ n) = ((x : R) ^ n)

Full source

@[simp, norm_cast]
theorem coe_pow (x : Ioc (0 : R) 1) (n : ℕ) : ↑(x ^ n) = ((x : R) ^ n) :=
  rfl

Power Operation Commutes with Embedding in $(0, 1]$ Interval

Informal description

For any element $x$ in the left-open right-closed interval $(0, 1]$ of a strict ordered semiring $R$ and any natural number $n$, the canonical embedding of $x^n$ into $R$ equals the $n$-th power of $x$ in $R$, i.e., $\overline{x^n} = x^n$.

Set.Ioc.semigroup instance

: Semigroup (Ioc (0 : R) 1)

Full source

instance semigroup : Semigroup (Ioc (0 : R) 1) := fast_instance%
  Subtype.coe_injective.semigroup _ coe_mul

Semigroup Structure on the Interval (0, 1] in Ordered Semirings

Informal description

For any strict ordered semiring $R$, the left-open right-closed interval $(0, 1]$ forms a semigroup under the multiplication operation inherited from $R$.

Set.Ioc.monoid instance

: Monoid (Ioc (0 : R) 1)

Full source

instance monoid : Monoid (Ioc (0 : R) 1) := fast_instance%
  Subtype.coe_injective.monoid _ coe_one coe_mul coe_pow

Monoid Structure on the Interval (0,1] in Ordered Semirings

Informal description

For any strict ordered semiring $R$, the left-open right-closed interval $(0,1]$ forms a monoid under the multiplication operation inherited from $R$, with $1$ as the multiplicative identity.

Set.Ioc.commSemigroup instance

{R : Type*} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] : CommSemigroup (Ioc (0 : R) 1)

Full source

instance commSemigroup {R : Type*} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] :
    CommSemigroup (Ioc (0 : R) 1) := fast_instance%
  Subtype.coe_injective.commSemigroup _ coe_mul

Commutative Semigroup Structure on (0, 1] in Strict Ordered Commutative Semirings

Informal description

For any commutative semiring $R$ with a partial order and the structure of a strict ordered ring, the left-open right-closed interval $(0, 1]$ forms a commutative semigroup under multiplication.

Set.Ioc.commMonoid instance

{R : Type*} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] : CommMonoid (Ioc (0 : R) 1)

Full source

instance commMonoid {R : Type*} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] :
    CommMonoid (Ioc (0 : R) 1) := fast_instance%
  Subtype.coe_injective.commMonoid _ coe_one coe_mul coe_pow

Commutative Monoid Structure on the Interval (0,1] in Strict Ordered Commutative Semirings

Informal description

For any commutative semiring $R$ with a partial order and the structure of a strict ordered ring, the left-open right-closed interval $(0, 1]$ forms a commutative monoid under multiplication.

Set.Ioc.cancelMonoid instance

{R : Type*} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [IsDomain R] : CancelMonoid (Ioc (0 : R) 1)

Full source

instance cancelMonoid {R : Type*} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [IsDomain R] :
    CancelMonoid (Ioc (0 : R) 1) :=
  { Set.Ioc.monoid with
    mul_left_cancel := fun a _ _ h =>
      Subtype.ext <| mul_left_cancel₀ a.prop.1.ne' <| (congr_arg Subtype.val h :)
    mul_right_cancel := fun _ b _ h =>
      Subtype.ext <| mul_right_cancel₀ b.prop.1.ne' <| (congr_arg Subtype.val h :) }

Cancellative Monoid Structure on (0,1] in Strict Ordered Domains

Informal description

For any ring $R$ with a partial order that forms a strict ordered ring and is a domain, the left-open right-closed interval $(0,1]$ forms a cancellative monoid under multiplication.

Set.Ioc.cancelCommMonoid instance

{R : Type*} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R] [IsDomain R] : CancelCommMonoid (Ioc (0 : R) 1)

Full source

instance cancelCommMonoid {R : Type*} [CommRing R] [PartialOrder R] [IsStrictOrderedRing R]
    [IsDomain R] :
    CancelCommMonoid (Ioc (0 : R) 1) :=
  { Set.Ioc.cancelMonoid, Set.Ioc.commMonoid with }

Cancellative Commutative Monoid Structure on (0,1] in Strict Ordered Domains

Informal description

For any commutative ring $R$ with a partial order that forms a strict ordered ring and is a domain, the left-open right-closed interval $(0,1]$ forms a cancellative commutative monoid under multiplication.

Set.Ioo.pos theorem

(x : Ioo (0 : R) 1) : 0 < (x : R)

Full source

theorem pos (x : Ioo (0 : R) 1) : 0 < (x : R) :=
  x.2.1

Positivity in Open Unit Interval: $0 < x$ for $x \in (0,1)$

Informal description

For any element $x$ in the open interval $(0, 1)$ of a partially ordered ring $R$, the value of $x$ is strictly greater than $0$.

Set.Ioo.lt_one theorem

(x : Ioo (0 : R) 1) : (x : R) < 1

Full source

theorem lt_one (x : Ioo (0 : R) 1) : (x : R) < 1 :=
  x.2.2

Upper Bound of Open Unit Interval: $x < 1$ for $x \in (0,1)$

Informal description

For any element $x$ in the open interval $(0, 1)$ of a partially ordered ring $R$, the value of $x$ is strictly less than $1$.

Set.Ioo.mul instance

: Mul (Ioo (0 : R) 1)

Full source

instance mul : Mul (Ioo (0 : R) 1) where
  mul p q :=
    ⟨p.1 * q.1, ⟨mul_pos p.2.1 q.2.1, mul_lt_one_of_nonneg_of_lt_one_right p.2.2.le q.2.1.le q.2.2⟩⟩

Multiplication on the Open Unit Interval

Informal description

The open interval $(0,1)$ in a partially ordered ring $R$ is equipped with a multiplication operation inherited from $R$.

Set.Ioo.coe_mul theorem

(x y : Ioo (0 : R) 1) : ↑(x * y) = (x * y : R)

Full source

@[simp, norm_cast]
theorem coe_mul (x y : Ioo (0 : R) 1) : ↑(x * y) = (x * y : R) :=
  rfl

Multiplication in Open Unit Interval Preserves Coefficients

Informal description

For any elements $x$ and $y$ in the open unit interval $(0,1)$ of a partially ordered ring $R$, the product $x * y$ in the interval equals the product $x * y$ in $R$.

Set.Ioo.semigroup instance

: Semigroup (Ioo (0 : R) 1)

Full source

instance semigroup : Semigroup (Ioo (0 : R) 1) := fast_instance%
  Subtype.coe_injective.semigroup _ coe_mul

Semigroup Structure on the Open Unit Interval

Informal description

For any strictly ordered semiring $R$, the open interval $(0,1)$ in $R$ forms a semigroup under multiplication inherited from $R$.

Set.Ioo.commSemigroup instance

{R : Type*} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] : CommSemigroup (Ioo (0 : R) 1)

Full source

instance commSemigroup {R : Type*} [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R] :
    CommSemigroup (Ioo (0 : R) 1) := fast_instance%
  Subtype.coe_injective.commSemigroup _ coe_mul

Commutative Semigroup Structure on the Open Unit Interval

Informal description

For any commutative semiring $R$ with a partial order and strict ordered ring structure, the open interval $(0,1)$ in $R$ forms a commutative semigroup under multiplication inherited from $R$.

Set.Ioo.one_sub_mem theorem

{t : β} (ht : t ∈ Ioo (0 : β) 1) : 1 - t ∈ Ioo (0 : β) 1

Full source

theorem one_sub_mem {t : β} (ht : t ∈ Ioo (0 : β) 1) : 1 - t ∈ Ioo (0 : β) 1 := by
  rw [mem_Ioo] at *
  refine ⟨sub_pos.2 ht.2, ?_⟩
  exact lt_of_le_of_ne ((sub_le_self_iff 1).2 ht.1.le) (mt sub_eq_self.mp ht.1.ne')

Closure of Open Unit Interval under One Minus Operation

Informal description

For any element $t$ in the open interval $(0,1)$ of an ordered semiring $\beta$, the element $1 - t$ also lies in $(0,1)$.

Set.Ioo.mem_iff_one_sub_mem theorem

{t : β} : t ∈ Ioo (0 : β) 1 ↔ 1 - t ∈ Ioo (0 : β) 1

Full source

theorem mem_iff_one_sub_mem {t : β} : t ∈ Ioo (0 : β) 1t ∈ Ioo (0 : β) 1 ↔ 1 - t ∈ Ioo (0 : β) 1 :=
  ⟨one_sub_mem, fun h => sub_sub_cancel 1 t ▸ one_sub_mem h⟩

Characterization of Elements in Open Unit Interval via One Minus Operation

Informal description

For any element $t$ in an ordered semiring $\beta$, $t$ belongs to the open interval $(0,1)$ if and only if $1 - t$ also belongs to $(0,1)$. In other words, $0 < t < 1 \leftrightarrow 0 < 1 - t < 1$.

Set.Ioo.one_minus_pos theorem

(x : Ioo (0 : β) 1) : 0 < 1 - (x : β)

Full source

theorem one_minus_pos (x : Ioo (0 : β) 1) : 0 < 1 - (x : β) := by simpa using x.2.2

Positivity of One Minus Element in Open Unit Interval

Informal description

For any element $x$ in the open interval $(0,1)$ of an ordered semiring $\beta$, the difference $1 - x$ is positive, i.e., $0 < 1 - x$.

Set.Ioo.one_minus_lt_one theorem

(x : Ioo (0 : β) 1) : 1 - (x : β) < 1

Full source

theorem one_minus_lt_one (x : Ioo (0 : β) 1) : 1 - (x : β) < 1 := by simpa using x.2.1

Subtraction from One in Open Unit Interval is Less Than One

Informal description

For any element $x$ in the open interval $(0,1)$ of an ordered semiring $\beta$, we have $1 - x < 1$.

Mathlib.Algebra.Order.Interval.Set.Instances

Main definitions

TODO