Set.image_update_Icc
theorem Set.image_update_Icc :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
(f : (i : ι) → α i) (i : ι) (a b : α i),
Function.update f i '' Set.Icc a b = Set.Icc (Function.update f i a) (Function.update f i b)
This theorem states that for any type `ι`, any function `α` from `ι` to another type, given a decidable equality on `ι` and a partial order on `α i` for each `i` in `ι`, for any function `f` from `ι` to `α i`, any index `i` in `ι`, and any `a` and `b` in `α i`, the image of the set of `f`'s values updated at index `i` over the closed interval `[a, b]` is the same as the closed interval between `f` updated at `i` with `a` and `f` updated at `i` with `b`.
In other words, if you update the value of the function at a certain point and then take the image of that function over a closed interval, it's the same as if you took the closed interval of the function with the updated values. This is a property related to the preservation of order and continuity after a function update.
More concisely: For any type `ι`, function `α : ι → Type`, decidable equality on `ι`, partial order on `α i` for each `i ∈ ι`, function `f : ι → α`, index `i ∈ ι`, and elements `a, b ∈ α i`, the image of `f` over the closed interval `[a, b]` is equal to the closed interval `[f i a, f i b]` in `α`.
|
Set.image_update_Ico
theorem Set.image_update_Ico :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
(f : (i : ι) → α i) (i : ι) (a b : α i),
Function.update f i '' Set.Ico a b = Set.Ico (Function.update f i a) (Function.update f i b)
This theorem states that for any function `f` from an index set `ι` to a family of partially ordered sets `α i`, where the equality in `ι` is decidable, and for any index `i` in `ι` and any two elements `a` and `b` from `α i`, the image under `f` of the left-closed right-open interval between `a` and `b` (denoted by `Set.Ico a b`) when `f` is updated at `i` is the same as the left-closed right-open interval between the updated values of `f` at `a` and `b`.
In simple terms, it's saying that when we update the function at a certain point and then calculate the image of the interval from `a` to `b`, it's the same as if we computed the interval of the updated function at `a` and `b`.
More concisely: Given a function `f` from an indexed set `ι` to a family of partially ordered sets `α i` with decidable equality, for any index `i` and elements `a` and `b` in `α i`, `Set.Ico a b ↦ f (Set.Ico a b) = Set.Ico (f a) (f b)`.
|
Set.image_update_uIcc
theorem Set.image_update_uIcc :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Lattice (α i)] [inst_1 : DecidableEq ι] (f : (i : ι) → α i)
(i : ι) (a b : α i),
Function.update f i '' Set.uIcc a b = Set.uIcc (Function.update f i a) (Function.update f i b)
This theorem states that for any type `ι`, any function `α : ι → Type u_2` that maps each element of `ι` to a type that forms a lattice, a decidable equality on `ι`, a function `f : ι → α i`, an index `i` in `ι`, and two elements `a` and `b` of `α i`, the image under the update function of the upper interval `uIcc a b` is the same as the upper interval formed by updating `f` at `i` with `a` and `b`. In simpler terms, updating the function's values at a point within a given interval and computing the image yields the same result as directly updating the interval endpoints.
More concisely: For any lattice-valued function `f` and decidable equality on type `ι`, the image under `f` of the upper interval `uIcc a b` is equal to the upper interval with endpoints updated to `f i a` and `f i b`.
|
Set.image_update_Ioo
theorem Set.image_update_Ioo :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
(f : (i : ι) → α i) (i : ι) (a b : α i),
Function.update f i '' Set.Ioo a b = Set.Ioo (Function.update f i a) (Function.update f i b)
The theorem `Set.image_update_Ioo` states that for any type `ι`, any indexed type `α : ι → Type`, and any type-dependent partial order over `α`, if we have a function `f : (i : ι) → α i` and an index `i : ι` along with two elements `a` and `b` of `α i`, then the image of the interval `(a, b)` under the function `f` updated at `i` is the interval `(f(i:=a), f(i:=b))`. This essentially means that if we update the function at a certain index, the set of values it takes between `a` and `b` remains the same interval when the function is updated at the same index with `a` and `b` respectively.
More concisely: For any type `ι`, indexed type `α : ι → Type`, partial order on `α`, function `f : ι → α`, index `i : ι`, and elements `a, b : α i`, the image of the interval `(a, b)` under `f` updated at `i` is the interval `(f(i:=a), f(i:=b))`.
|
Set.Icc_diff_pi_univ_Ioc_subset
theorem Set.Icc_diff_pi_univ_Ioc_subset :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → LinearOrder (α i)]
(x y z : (i : ι) → α i),
(Set.Icc x z \ Set.univ.pi fun i => Set.Ioc (y i) (z i)) ⊆ ⋃ i, Set.Icc x (Function.update z i (y i))
This theorem states that for any three functions `x`, `y`, `z` that are indexed over the same type `ι` and map to types `α i`, the set difference between the closed box `[x, z]` and the product of the open-closed intervals `(y i, z i]` for all `i` is contained within the union of the closed boxes `[x, update z i (y i)]` for all `i`. In simpler terms, if we consider each `α i` as a dimension, then the "volume" between a closed box and the product of half-open intervals is covered by the union of certain closed boxes. As a specific case, when `x = y`, the theorem tells us that the difference between a closed box `[x, y]` and the product of half-open intervals `{z | ∀ i, x i < z i ≤ y i}` is covered by the union of the "faces" of `[x, y]` that are adjacent to `x`.
More concisely: For functions indexed over the same type with values in different types, the set difference between a closed box and the product of open-closed intervals is contained in the union of the closed boxes obtained by updating the larger function with the smaller one at each index.
|
Set.pi_univ_Ici
theorem Set.pi_univ_Ici :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] (x : (i : ι) → α i),
(Set.univ.pi fun i => Set.Ici (x i)) = Set.Ici x
This theorem states that for any index set `ι` and a family of sets `α`, where each `α i` is preordered, and for any function `x : ι → α i`, the set of all dependent functions that for every index `i` map to an element greater or equal to `x i` is the same as the set of all functions greater or equal to `x`. In other words, the left-closed right-infinite interval of the universal set of dependent functions, where each function maps to a value equal or greater than the corresponding value in `x`, equals the left-closed right-infinite interval starting at `x`.
More concisely: For any indexed family of preordered sets `α i` and function `x : ι → α i`, the set of functions `f : ι → α i` with `i in ι` implying `f i ≥ x i` equals the set of functions greater than or equal to `x`.
|
Set.pi_univ_Icc
theorem Set.pi_univ_Icc :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] (x y : (i : ι) → α i),
(Set.univ.pi fun i => Set.Icc (x i) (y i)) = Set.Icc x y
This theorem states that for any type `ι`, any function `α` from `ι` to some type, and any two functions `x` and `y` from `ι` to the type determined by `α`, the set of all functions from `ι` to `α` such that for each `i` in `ι`, the function value is in the closed interval from `x(i)` to `y(i)`, is exactly the set of all functions from `ι` to `α` that lie in the closed interval from `x` to `y`. This is essentially stating that the product of intervals is an interval, generalised to an arbitrary index set `ι` and arbitrary preorders on each coordinate.
More concisely: For any type `ι` and preorders on `ι` and a type `α`, the set of functions from `ι` to `α` with values in the closed interval between `x(i)` and `y(i)` for all `i` equals the set of functions from `ι` to `α` with values in the closed interval between `x` and `y`.
|
Set.Icc_diff_pi_univ_Ioo_subset
theorem Set.Icc_diff_pi_univ_Ioo_subset :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → LinearOrder (α i)]
(x y x' y' : (i : ι) → α i),
(Set.Icc x y \ Set.univ.pi fun i => Set.Ioo (x' i) (y' i)) ⊆
(⋃ i, Set.Icc x (Function.update y i (x' i))) ∪ ⋃ i, Set.Icc (Function.update x i (y' i)) y
This theorem states that if `x`, `y`, `x'`, and `y'` are functions mapping an index `i : ι` to `α i`, then the set difference between the box `[x, y]` and the product of the open intervals `(x' i, y' i)` for each `i` is contained within the union of certain boxes. Specifically, for each index `i : ι`, we consider the boxes `[x, update y i (x' i)]` and `[update x i (y' i), y]`, and take their union.
In simpler terms, if `x' = x` and `y' = y`, the theorem asserts that the difference between a closed box `[x, y]` and the corresponding open box `{z | ∀ i, x i < z i < y i}` is covered by the union of the faces of `[x, y]`. In such a case, the faces of the box `[x, y]` are the boxes obtained by replacing either the lower or upper endpoint of the box with the corresponding endpoint of the open interval.
More concisely: Given functions `x`, `y`, `x'`, and `y'` mapping an index `ι` to `α i`, the set difference between the box `[x, y]` and the product of open intervals `(x' i, y' i)` for each `i` is contained in the union of the boxes `[x, update y i (x' i)]` and `[update x i (y' i), y]` for all `i`.
|
Set.pi_univ_Ioi_subset
theorem Set.pi_univ_Ioi_subset :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] (x : (i : ι) → α i) [inst_1 : Nonempty ι],
(Set.univ.pi fun i => Set.Ioi (x i)) ⊆ Set.Ioi x
The theorem `Set.pi_univ_Ioi_subset` states that for any index type `ι`, any family of types `α` indexed by `ι` where each type `α i` is a preorder, and any dependent function `x : Π i, α i`, the set of all dependent functions `f` such that `f a` is greater than `x a` for all `a` in the universe of `ι` is a subset of the set of all dependent functions `g` such that `g` is greater than `x`. It requires the condition that `ι` is a nonempty type.
In other words, the left-open right-infinite intervals of each `α i` defined by `x i` combine to form a subset of the left-open right-infinite interval of the dependent functions defined by `x`.
More concisely: For any nonempty index type `ι` and family `α i` of preorders indexed by `ι` with dependent function `x : Π i, α i`, the set of functions `f` such that `f a > x a` for all `a : ι` is a subset of the set of functions `g` such that `g > x`.
|
Set.image_update_Ioc
theorem Set.image_update_Ioc :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
(f : (i : ι) → α i) (i : ι) (a b : α i),
Function.update f i '' Set.Ioc a b = Set.Ioc (Function.update f i a) (Function.update f i b)
The theorem `Set.image_update_Ioc` states that for any index type `ι`, any indexed type `α`, any decidable equality on `ι`, and any partial order on `α`, given a function `f` that maps from `ι` to `α`, and two values `a` and `b` from `α i`, the image of the interval `(a, b]` (exclusive of `a`, inclusive of `b`) under the update of `f` at index `i` is the interval `(f(i) updated with a, f(i) updated with b]`. In simpler terms, it means that updating a function at a particular index and then taking the image of an interval under this updated function gives the same result as first taking the images of the endpoints under the updated function and then forming the interval.
More concisely: For any index type `ι`, any indexed type `α` with decidable equality, any partial order on `α`, and any function `f : ι → α`, the image of the interval `(f i)↑[a, b]` under `f.update i a` is equal to `(f i)↑[f a, f b]`. (Here, `↑` denotes the image under a function, `update` is the update operator in Lean, and `[a, b]` denotes the interval from `a` to `b` inclusive.)
|
Set.pi_univ_Iio_subset
theorem Set.pi_univ_Iio_subset :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] (x : (i : ι) → α i) [inst_1 : Nonempty ι],
(Set.univ.pi fun i => Set.Iio (x i)) ⊆ Set.Iio x
The theorem `Set.pi_univ_Iio_subset` states that for any type `ι`, any family of types `α` indexed by `ι`, any preorder structure on each `α i`, and any function `x` from `ι` to `α i` (i.e., an element of the dependent product type), if `ι` is nonempty, then the set of dependent functions that are strictly less than `x` at each index is a subset of the set of dependent functions that are strictly less than `x` in the sense of the product order. In other words, if every coordinate of a function is less than the corresponding coordinate of `x`, then the function itself is less than `x` in the preorder of functions.
More concisely: For any nonempty type `ι`, family of types `α i` indexed by `ι`, preorder `≤_α i` on each `α i`, and function `x : ∏ i, α i` from `ι` to `α i`, the subset of dependent functions `g : ∏ i, α i` with `g i < x i` for all `i` is included in the subset of functions `h : ∏ i, α i` with `h < x` in the product order.
|