AddConstMapClass.map_sub_nsmul
theorem AddConstMapClass.map_sub_nsmul :
∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} {a : G} {b : H} [inst : AddGroup G] [inst_1 : AddGroup H]
[inst_2 : AddConstMapClass F G H a b] (f : F) (x : G) (n : ℕ), f (x - n • a) = f x - n • b
This theorem states that for every types `F`, `G`, `H`, an element `a` in `G`, an element `b` in `H`, with `G` and `H` being AddGroups, and a `AddConstMapClass` instance for `F`, `G`, `H`, `a`, `b`, the map `f` from `F` to `G` has the property that for any `x` in `G` and any natural number `n`, applying `f` to the difference of `x` and `n` times `a` equals the difference of `f(x)` and `n` times `b`. In terms of mathematical notation, for all `f : F -> G`, `x : G`, and `n : ℕ`, we have `f(x - n*a) = f(x) - n*b`.
More concisely: For any AddGroups G, H, types F with an AddConstMapClass instance, elements a in G, b in H, and functions f : F -> G, we have f(x - na) = f(x) - nb for all x in G and natural numbers n.
|
AddConstMap.map_add_const'
theorem AddConstMap.map_add_const' :
∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (self : AddConstMap G H a b)
(x : G), self.toFun (x + a) = self.toFun x + b
This theorem states that for any given types `G` and `H` with addition defined on them, and any given `a` of type `G` and `b` of type `H`, an `AddConstMap` from `G` to `H` with constants `a` and `b` has the property that applying the map's function to `x + a` (where `x` is some element of `G`) results in the same output as applying the function to `x` and then adding `b`. This theorem suggests using `map_add_const` instead.
More concisely: For any types `G` and `H` with addition, and `a:G` and `b:H`, the `AddConstMap` from `G` to `H` with constants `a` and `b` satisfies `(f map x) + b = f (x + a)` for all `x:G`.
|
AddConstMapClass.map_add_const
theorem AddConstMapClass.map_add_const :
∀ {F : Type u_1} {G : outParam (Type u_2)} {H : outParam (Type u_3)} [inst : Add G] [inst_1 : Add H]
{a : outParam G} {b : outParam H} [self : AddConstMapClass F G H a b] (f : F) (x : G), f (x + a) = f x + b
This theorem establishes a property for a particular class of function maps, denoted as `AddConstMapClass`. For any types `F`, `G`, and `H`, where `G` and `H` are equipped with addition (`Add`), and any elements `a` of type `G`, `b` of type `H`, and a map `f` of type `F` belonging to `AddConstMapClass` with parameters `a` and `b`, the theorem claims that applying `f` to `x + a` (for any `x` of type `G`) results in the same output as applying `f` to `x` and then adding `b`. In other words, the map `f` semi-conjugates the operation of "shifting by `a`" in its domain to the operation of "shifting by `b`" in its codomain. This is expressed as `∀ x, f (x + a) = f x + b`.
More concisely: For any `AddConstMapClass` map `f` with parameters `a` in the domain type `G` and `b` in the codomain type, and for all `x` in `G`, we have `f (x + a) = f x + b`.
|
AddConstMapClass.map_add_nat'
theorem AddConstMapClass.map_add_nat' :
∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} {b : H} [inst : AddMonoidWithOne G] [inst_1 : AddMonoid H]
[inst_2 : AddConstMapClass F G H 1 b] (f : F) (x : G) (n : ℕ), f (x + ↑n) = f x + n • b
This theorem states that for any types `F`, `G`, and `H`, given an element `b` of type `H`, an `AddMonoidWithOne` instance for `G`, an `AddMonoid` instance for `H`, and an `AddConstMapClass` instance for `F`, `G`, `H` with `1` and `b`, for any function `f` from `F` to `G`, any element `x` of `G`, and any natural number `n`, the function `f` applied to the sum of `x` and the natural number `n` (coerced to `G`) is equal to the sum of `f` applied to `x` and `n` multiplied by `b` (using scalar multiplication).
More concisely: For any types `F`, `G`, and `H`, given an `AddMonoidWithOne` `b` in `H`, `AddMonoid` structures on `G` and `H`, and an `AddConstMapClass` for `F`, `G`, `H` with `1` and `b`, for any function `f` from `F` to `G`, `x` in `G`, and natural number `n`, we have `f(x + n) = f(x) + n * b`.
|
AddConstMapClass.rel_map_of_Icc
theorem AddConstMapClass.rel_map_of_Icc :
∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} {a : G} {b : H} [inst : LinearOrderedAddCommGroup G]
[inst_1 : Archimedean G] [inst_2 : AddGroup H] [inst_3 : AddConstMapClass F G H a b] {f : F} {R : H → H → Prop}
[inst_4 : IsTrans H R] [hR : CovariantClass H H (fun x y => y + x) R],
0 < a →
∀ {l : G},
(∀ x ∈ Set.Icc l (l + a), ∀ y ∈ Set.Icc l (l + a), x < y → R (f x) (f y)) →
((fun x x_1 => x < x_1) ⇒ R) ⇑f ⇑f
This theorem, titled "Auxiliary lemmas for the 'monotonicity on a fundamental interval implies monotonicity' lemmas", is a fundamental statement about monotonic functions and intervals, and it is specified for any given relation to make it applicable for both Monotone and StrictMono scenarios. It states that given an ordered additive group `G`, an Archimedean property on `G`, an additive group `H`, a constant mapping class from `F` to `G` to `H` with constants `a` and `b`, a function `f` from `F` and a relation `R` on `H` that is transitive and covariant under addition, if `a > 0`, then for any value `l` in `G`, if for all `x` and `y` in the closed interval from `l` to `l + a`, where `x < y`, `R` holds for `f(x)` and `f(y)`, it implies that the same relation `R` holds for `f` for any two arguments such that the first is less than the second.
More concisely: Given an Archimedean additive group G, a transitive and covariant relation R on an additive group H, a monotonic function f from a set F to H with constants a and b, if for all x, y in the closed interval [l, l+a] in G with x < y, R holds between f(x) and f(y), then R holds between f(x) and f(y) for all x, y in F with x < y.
|
AddConstMapClass.map_add_nsmul
theorem AddConstMapClass.map_add_nsmul :
∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} {a : G} {b : H} [inst : AddMonoid G] [inst_1 : AddMonoid H]
[inst_2 : AddConstMapClass F G H a b] (f : F) (x : G) (n : ℕ), f (x + n • a) = f x + n • b
This theorem states that for any types `F`, `G`, and `H`, any elements `a` of `G`, `b` of `H`, and given that `G` and `H` are `AddMonoid`s and there exists `AddConstMapClass` between `F`, `G` and `H` with `a` and `b`, for any `f` from `F`, `x` from `G` and `n` from natural numbers, applying `f` to the addition of `x` and `n` times `a` is equal to the addition of `f(x)` and `n` times `b`. In mathematical terms, this theorem asserts that $f(x + n \cdot a) = f(x) + n \cdot b$ under the specified conditions.
More concisely: For any AddMonoid types F, G, H with an AddConstMapClass between F, G, and H, and elements a in G, b in H, and natural number n, the map f from F satisfies f(x + na) = f(x) + nb for all x in G.
|
AddConstMapClass.map_add_zsmul
theorem AddConstMapClass.map_add_zsmul :
∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} {a : G} {b : H} [inst : AddGroup G] [inst_1 : AddGroup H]
[inst_2 : AddConstMapClass F G H a b] (f : F) (x : G) (n : ℤ), f (x + n • a) = f x + n • b
This theorem states that for any three types `F`, `G`, and `H`, along with elements `a` of type `G`, `b` of type `H`, an integer `n`, a function `f` from `F` to `G`, and `x` of type `G`, if `G` and `H` are add groups and there is a map from `F` to `G` to `H` that maps `a` to `b`, then applying the function `f` to the sum of `x` and `n` times `a` is the same as the sum of `f(x)` and `n` times `b`. In mathematical notation, this would be expressed as: `f(x + n*a) = f(x) + n*b`.
More concisely: For any add groups G, H, types F, functions f from F to G to H with f(a) = b, and elements a of type F, x of type G, and integer n, we have f(x + n*a) = f(x) + n*b.
|