Set.Ioc.le_one
theorem Set.Ioc.le_one :
∀ {α : Type u_1} [inst : StrictOrderedSemiring α] [inst_1 : Nontrivial α] {t : ↑(Set.Ioc 0 1)}, t ≤ 1
This theorem, `Set.Ioc.le_one`, states that for any strict ordered semiring `α` with nontrivial elements, any element `t` inside the left-open right-closed interval from 0 to 1 (denoted by `Set.Ioc 0 1`), is less than or equal to 1. Here, `StrictOrderedSemiring` is a type of ordered semiring where the ordering and the binary operation '+' are compatible in a certain way, and `Nontrivial` means that the type `α` has at least two distinct elements.
More concisely: For any strict ordered semiring with nontrivial elements, every element in the left-open right-closed interval [0, 1) is less than or equal to 1.
|
Set.Icc.coe_one
theorem Set.Icc.coe_one : ∀ {α : Type u_1} [inst : OrderedSemiring α], ↑1 = 1
This theorem states that for any type `α` which has an ordered semiring structure, the set interval closure of 1 (denoted as `↑1`) is equal to 1. In other words, in any ordered semiring, the singleton set containing 1 can be identified with 1 itself.
More concisely: In any ordered semiring, the set interval closure of 1 equals 1.
|
Set.Icc.coe_zero
theorem Set.Icc.coe_zero : ∀ {α : Type u_1} [inst : OrderedSemiring α], ↑0 = 0
This theorem states that for any type `α` which is an ordered semiring, the coercion of the integer zero to this type equals the zero element of the semiring. In other words, when you take the integer zero and convert it into any instance of an ordered semiring (`α`), it remains the zero element in that semiring.
More concisely: For any ordered semiring `α`, the coerced integer zero is equal to the semiring's additive identity.
|
Set.Icc.coe_pow
theorem Set.Icc.coe_pow : ∀ {α : Type u_1} [inst : OrderedSemiring α] (x : ↑(Set.Icc 0 1)) (n : ℕ), ↑(x ^ n) = ↑x ^ n
This theorem states that for any type `α` which is an ordered semiring, and any element `x` in the closed interval from 0 to 1 of type `α`, the `n`-th power of `x` (where `n` is a natural number) is equal to `x` raised to the power `n`. Note that the elements `x` and `x^n` are both in the interval from 0 to 1, evidenced by the fact that they are taken as elements of the set `Set.Icc 0 1`. The `↑` symbol in the theorem denotes the coercion from the set `Set.Icc 0 1` to the type `α`.
More concisely: For any ordered semiring type `α` and element `x` in the closed interval `[0, 1]` of type `α`, the `n`-th power of `x` equals `x` raised to the power `n`.
|
Set.Ico.nonneg
theorem Set.Ico.nonneg :
∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : Nontrivial α] {t : ↑(Set.Ico 0 1)}, 0 ≤ t
The theorem `Set.Ico.nonneg` states that for any type `α` that is an ordered semiring and is nontrivial, if `t` is an element of the left-closed right-open interval from `0` to `1` (i.e., `t` is in the set `Set.Ico 0 1`), then `t` is greater than or equal to `0`. This essentially means that all elements in the interval [0, 1) are nonnegative.
More concisely: For any nontrivial ordered semiring type `α`, all elements in the left-closed right-open interval `[0, 1)` have a non-negative value.
|
Set.Icc.coe_mul
theorem Set.Icc.coe_mul : ∀ {α : Type u_1} [inst : OrderedSemiring α] (x y : ↑(Set.Icc 0 1)), ↑(x * y) = ↑x * ↑y := by
sorry
The theorem `Set.Icc.coe_mul` states that for any ordered semiring `α`, and for any `x` and `y` in the closed interval from 0 to 1 denoted by `Set.Icc 0 1`, the product of `x` and `y` is equal to the product of the values `x` and `y` point to. This is an equality in the context of using the coe function (↑) to remove or upgrade the type of `x`, `y` and their product from the interval `Set.Icc 0 1` to the underlying type `α`. In mathematical terms, given an ordered semiring, the product of any two elements in the closed interval [0,1] remains the same when considered in the broader context of the semiring.
More concisely: For any ordered semiring α, the product of two elements in the closed interval [0,1] equals their pointwise product in α.
|
Set.Icc.le_one
theorem Set.Icc.le_one : ∀ {α : Type u_1} [inst : OrderedSemiring α] {t : ↑(Set.Icc 0 1)}, t ≤ 1
The theorem `Set.Icc.le_one` states that for any type `α` that is an ordered semiring, any element `t` that belongs to the interval `Icc (0:α) 1` (including the bounds 0 and 1), it is true that `t ≤ 1`. This theorem essentially asserts that any number in the closed interval from 0 to 1 in an ordered semiring is less than or equal to 1.
More concisely: For any ordered semiring type `α` and any element `t` in the interval `Icc (0:α) 1`, we have `t ≤ 1`.
|
Set.Icc.nonneg
theorem Set.Icc.nonneg : ∀ {α : Type u_1} [inst : OrderedSemiring α] {t : ↑(Set.Icc 0 1)}, 0 ≤ t
The theorem `Set.Icc.nonneg` states that for any type `α` that is an ordered semiring, for every element `t` in the set which is the closed interval from `0` to `1` (i.e., `t` lies in the set of `α` where `a` and `b` are such that `0 ≤ a ≤ b ≤ 1`), `t` is non-negative, i.e., `0 ≤ t`. In other words, the theorem asserts that all elements in a closed interval from `0` to `1` in an ordered semiring are greater than or equal to `0`.
More concisely: For any ordered semiring type `α`, the element `t` in the interval `[0, 1]` satisfies `0 ≤ t`.
|