Set.IccExtend_of_mem
theorem Set.IccExtend_of_mem :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a b : α} (h : a ≤ b) {x : α} (f : ↑(Set.Icc a b) → β)
(hx : x ∈ Set.Icc a b), Set.IccExtend h f x = f ⟨x, hx⟩
The theorem `Set.IccExtend_of_mem` states that for any types `α` and `β` where `α` has a linear order, any two values `a` and `b` from `α` with `a ≤ b`, any function `f` from the interval `[a, b]` to `β`, and any value `x` from `α` within the interval `[a, b]`, the value of the function `f` extended over all of `α` at `x` (`Set.IccExtend h f x`) is the same as the value of `f` at `x` (`f { val := x, property := hx }`). In other words, if you extend a function defined on a closed interval to all of `α`, the values on the original interval remain unchanged.
More concisely: For any type with a linear order, any function defined on an interval is unchanged when extended to the entire type at points within the interval.
|
Set.projIcc_val
theorem Set.projIcc_val :
∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} (h : a ≤ b) (x : ↑(Set.Icc a b)), Set.projIcc a b h ↑x = x := by
sorry
This theorem states that for any type `α` that has a linear order, given any two elements `a` and `b` of type `α` such that `a` is less than or equal to `b`, and any element `x` from the closed interval between `a` and `b`, the projection of `x` from `α` onto the closed interval `[a, b]` equals `x` itself. This means that for any element in the closed interval, the process of projecting it onto the interval does not change its value.
More concisely: For any linear order type `α` and elements `a ≤ b` within it, the projection of any `x ∈ [a, b]` onto the interval `[a, b]` equals `x` itself.
|
Set.projIic_of_mem
theorem Set.projIic_of_mem :
∀ {α : Type u_1} [inst : LinearOrder α] {b x : α} (hx : x ∈ Set.Iic b), Set.projIic b x = ⟨x, hx⟩
This theorem states that for any type `α` equipped with a linear order, and for any elements `b` and `x` of type `α` where `x` belongs to the set `Set.Iic b` (which represents the left-infinite right-closed interval `(-∞, b]`), the projection of `x` onto the interval `(-∞, b]` using the `Set.projIic` function yields `x` itself. In other words, if `x` is already in the interval `(-∞, b]`, its projection onto this interval does not change its value.
More concisely: For any type `α` with a linear order, and any `b` in `α` and `x` in the interval `(-∞, b]`, the projection of `x` onto `(-∞, b]` using `Set.projIic` equals `x`.
|
Set.projIcc.proof_1
theorem Set.projIcc.proof_1 :
∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), a ≤ b → ∀ (x : α), a ≤ max a (min b x) ∧ max a (min b x) ≤ b
This theorem states that for any type `α` that has a linear order, given two elements `a` and `b` of that type such that `a` is less than or equal to `b`, then for any element `x` of the same type, the maximum of `a` and the minimum of `b` and `x` is both greater than or equal to `a` and less than or equal to `b`. Essentially, it is asserting that for any `x`, when it is constrained to be within the interval [a, b] via min and max operations, it indeed stays within that interval.
More concisely: For any linear order type `α` and elements `a`, `b`, and `x` of type `α` with `a ≤ b`, the minimum of `b` and the maximum of `a` and `x` lies within the interval [`a`, `b`].
|
Set.monotone_projIcc
theorem Set.monotone_projIcc :
∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} (h : a ≤ b), Monotone (Set.projIcc a b h)
This theorem states that for any type `α` equipped with a linear order, and any two elements `a` and `b` of `α` such that `a` is less than or equal to `b`, the function that projects `α` to the closed interval `[a, b]` is monotone. That is, if `x` and `y` are any two elements in `α` such that `x` is less than or equal to `y`, applying this projection function to `x` and `y` maintains the order; the output of the function applied to `x` is less than or equal to the function applied to `y`.
More concisely: For any linear order `α` and elements `a ≤ b` in `α`, the function that maps an element `x` to the closed interval `[a, b]` is monotone, i.e., `x ≤ y` implies `[a, b] x ≤ [a, b] y`.
|
Set.IccExtend_val
theorem Set.IccExtend_val :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a b : α} (h : a ≤ b) (f : ↑(Set.Icc a b) → β)
(x : ↑(Set.Icc a b)), Set.IccExtend h f ↑x = f x
The theorem `Set.IccExtend_val` states that for any types `α` and `β` where `α` has a LinearOrder structure, for any elements `a` and `b` of `α` where `a ≤ b`, and any function `f` from the closed interval `[a, b]` to `β`, the value of the function `f` at any point `x` within the interval `[a, b]` remains the same even when the function `f` is extended to the entire domain `α` using `Set.IccExtend`. In other words, the extension of the function `f` to the whole domain `α` using `Set.IccExtend` does not affect the values of `f` within the interval `[a, b]`.
More concisely: For any type `α` with a LinearOrder structure, any `a ≤ b` in `α`, and any function `f` from the interval `[a, b]` to a type `β`, the value `f x` is equal to the value of the extension of `f` by `Set.IccExtend at x` for all `x` in `[a, b]`.
|
Set.projIcc_of_le_left
theorem Set.projIcc_of_le_left :
∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} (h : a ≤ b) {x : α}, x ≤ a → Set.projIcc a b h x = ⟨a, ⋯⟩ := by
sorry
The theorem `Set.projIcc_of_le_left` states that for any types `α` that has a linear order, given two elements `a` and `b` in `α` where `a` is less than or equal to `b`, and any element `x` in `α` that is less than or equal to `a`, the projection of `x` onto the closed interval `[a, b]` will be `a`. In other words, if `x` is outside the interval to the left, it gets projected to the left endpoint `a`.
More concisely: For any type `α` with a linear order, and elements `a ≤ b` in `α` and `x ≤ a`, the projection of `x` onto the interval `[a, b]` is equal to `a`.
|
Set.projIcc_of_right_le
theorem Set.projIcc_of_right_le :
∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} (h : a ≤ b) {x : α}, b ≤ x → Set.projIcc a b h x = ⟨b, ⋯⟩ := by
sorry
This theorem states that for any type `α` with a linear order, given two elements `a` and `b` such that `a` is less than or equal to `b`, and any element `x` of `α`, if `b` is less than or equal to `x`, then the projection of `x` onto the closed interval `[a, b]` is equal to `b`. This essentially means that any element greater than or equal to `b` gets mapped to `b` when projected onto the interval `[a, b]`.
More concisely: For any linear order `α`, if `a ≤ b` in `α` and `x ∈ α` with `b ≤ x`, then the projection of `x` onto the interval `[a, b]` equals `b`.
|
Set.IccExtend_of_right_le
theorem Set.IccExtend_of_right_le :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a b : α} (h : a ≤ b) {x : α} (f : ↑(Set.Icc a b) → β),
b ≤ x → Set.IccExtend h f x = f ⟨b, ⋯⟩
This theorem states that for any types `α` and `β` with `α` having a linear order, given two values `a` and `b` in `α` such that `a` is less than or equal to `b`, a function `f` from the closed interval `[a, b]` to `β`, and a value `x` in `α`, if `b` is less than or equal to `x`, then the extension of the function `f` to the entire set `α`, when evaluated at `x`, equals the evaluation of `f` at `b`. This implies that the extension of the function `f` is constant for all `x` greater than `b`.
More concisely: For any function `f` from a linearly ordered type `α` to a type `β`, and any `a ≤ b` in `α` with `x ≥ b`, the extension of `f` to `α` evaluates `f x = f b`.
|
Set.IccExtend_eq_self
theorem Set.IccExtend_eq_self :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a b : α} (h : a ≤ b) (f : α → β),
(∀ x < a, f x = f a) → (∀ (x : α), b < x → f x = f b) → Set.IccExtend h (f ∘ Subtype.val) = f
This theorem states that given a function `f : α → β` that is constant on intervals `(-∞, a]` and `[b, +∞)`, where `α` is a type with a linear order and `a ≤ b`, the extension of this function from the closed interval `[a, b]` to the whole line is equal to the original function. In other words, if a function takes the same value `f a` for all inputs `x < a` and the same value `f b` for all inputs `x > b`, then extending this function to all of `α` using `Set.IccExtend` will result in the same function `f`.
More concisely: If a function `f : α → β` is constant on the intervals `(-\infty, a]` and `[b, +∞)` for `α` a linearly ordered type with `a ≤ b`, then `Set.IccExtend f (Icc a b α) = f`.
|
Set.projIcc_of_mem
theorem Set.projIcc_of_mem :
∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} (h : a ≤ b) {x : α} (hx : x ∈ Set.Icc a b),
Set.projIcc a b h x = ⟨x, hx⟩
The theorem `Set.projIcc_of_mem` states that for any type `α` equipped with a linear order, and for any two elements `a` and `b` in `α` where `a` is less than or equal to `b`, if an element `x` belongs to the closed interval from `a` to `b` (denoted by `Set.Icc a b`), then the projection of `x` onto the same interval (`Set.projIcc a b h x`) is the same as the pair consisting of `x` along with the proof that `x` is in the interval `Set.Icc a b`. In other words, if `x` is already in the interval, its projection to the interval is just itself.
More concisely: For any type `α` with a linear order and elements `a ≤ b`, if `x ∈ Set.Icc a b`, then `Set.projIcc a b x = (x, ⟨h: x ∈ Set.Icc a b⟩)`.
|
Set.projIci_of_mem
theorem Set.projIci_of_mem :
∀ {α : Type u_1} [inst : LinearOrder α] {a x : α} (hx : x ∈ Set.Ici a), Set.projIci a x = ⟨x, hx⟩
The theorem `Set.projIci_of_mem` states that for any type `α` with a linear order, and for any elements `a` and `x` of `α`, if `x` belongs to the left-closed right-infinite interval starting at `a` (i.e., `x` is in the set of all elements greater than or equal to `a`), then the projection of `x` onto this interval (which maps `x` to the maximum of `a` and `x`) is equal to `x` itself. The projection of `x` into this set is represented as a dependent pair with `x` as its value and the proof of `x` belonging to the interval as its property. This essentially means that if `x` is already in the interval `[a, ∞)`, its projection onto this interval is simply `x` itself.
More concisely: For any type with a linear order and any element `x` greater than or equal to `a`, the projection of `x` onto the interval `[a, ∞)` is equal to `x`.
|
Set.projIci_coe
theorem Set.projIci_coe : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α} (x : ↑(Set.Ici a)), Set.projIci a ↑x = x := by
sorry
This theorem states that for any type `α` equipped with a linear order, and any `a` of type `α`, the projection onto the closed interval `[a, ∞)` of any element `x` in the set `Set.Ici a` (which represents the interval `[a, ∞)`) is equal to `x` itself. In other words, for all members of the interval `[a, ∞)`, projecting them onto the interval `[a, ∞)` doesn't change their value.
More concisely: For any type `α` with a linear order, and for all `a` in `α` and `x` in the set `Set.Ici a` (the closed interval `[a, ∞)`), the projection of `x` onto the interval `[a, ∞)` equals `x` itself.
|
Set.projIic_coe
theorem Set.projIic_coe : ∀ {α : Type u_1} [inst : LinearOrder α] {b : α} (x : ↑(Set.Iic b)), Set.projIic b ↑x = x := by
sorry
This theorem states that for any type `α` equipped with a linear order, and for any element `b` from `α`, the projection of any element `x` from the left-infinite right-closed interval `(-∞, b]` (denoted as `Set.Iic b`), back onto itself via the `Set.projIic` function, yields the original element `x` itself. In other words, the `Set.projIic` function acts as an identity on the elements of the interval `(-∞, b]`.
More concisely: For any type `α` with a linear order and any `b` in `α`, the `Set.projIic` function maps elements in the left-infinite right-closed interval `(-∞, b]` to themselves.
|
Set.IccExtend_of_le_left
theorem Set.IccExtend_of_le_left :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a b : α} (h : a ≤ b) {x : α} (f : ↑(Set.Icc a b) → β),
x ≤ a → Set.IccExtend h f x = f ⟨a, ⋯⟩
This theorem states that for all types `α` and `β` with `α` having a linear order, and for all `a`, `b`, `x` of type `α` and a function `f` from the closed interval `[a, b]` to `β` (`↑(Set.Icc a b)` denotes the closed interval [a, b]), if `a` is less than or equal to `b` and `x` is less than or equal to `a`, then the value of the extension of function `f` to `α` at `x` is equal to the value of `f` at `a`. In other words, for a function extended from a closed interval to the entire line, the function values outside the left end of the interval are equal to the function value at the left end.
More concisely: For all types `α` with a linear order, and for all functions `f` from the closed interval `[a, b]` of type `α` to another type `β`, if `a ≤ b` and `x ≤ a`, then `f.extend a x = f a`.
|