AddUnits.inducing_embedProduct
theorem AddUnits.inducing_embedProduct :
∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddMonoid M], Inducing ⇑(AddUnits.embedProduct M)
The theorem `AddUnits.inducing_embedProduct` states that for any type `M` which has a topology and an additive monoid structure, the map `AddUnits.embedProduct M` is an inducing function. In topology, an inducing function is one that pulls back the topology from the codomain to the domain, making the topology of the domain the initial topology with respect to that function. In this case, the function `AddUnits.embedProduct M` carries the topology from the product of `M` and the opposite of `M` back to `AddUnits M`.
More concisely: The `AddUnits.embedProduct` map of a topological additive monoid `M` is a topology-preserving embedding.
|
AddUnits.continuous_val
theorem AddUnits.continuous_val :
∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddMonoid M], Continuous AddUnits.val
The theorem `AddUnits.continuous_val` states that for any type `M` that has a topological space structure and an addition monoid structure, the function `AddUnits.val` (which extracts the underlying value from an `AddUnits` object in the base `AddMonoid`) is continuous. In simpler terms, this says that in the context of topological spaces and addition monoids, we can map from `AddUnits` to their underlying values without breaking continuity, i.e., without introducing any gaps or jumps.
More concisely: The function extracting the underlying value from an `AddUnits` object in a topological space with an addition monoid structure is continuous.
|
Units.continuous_val
theorem Units.continuous_val : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Monoid M], Continuous Units.val
This theorem states that for any type `M`, given that `M` has a topological space structure and a monoid structure, the value function on units of `M` (which retrieves the underlying value in the base monoid) is continuous. This essentially means that the elements of `M` behave nicely under the operation of monoid in the topological sense, that is, the 'closeness' relations in `M` are preserved under the monoid operation.
More concisely: If `M` is a type with both a topological space and a monoid structure, then the value function on units of `M` is continuous.
|
AddUnits.continuous_iff
theorem AddUnits.continuous_iff :
∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [inst_2 : TopologicalSpace X]
{f : X → AddUnits M}, Continuous f ↔ Continuous (AddUnits.val ∘ f) ∧ Continuous fun x => ↑(-f x)
The theorem `AddUnits.continuous_iff` states that for any types `M` and `X` where `M` is both a topological space and an additive monoid, and `X` is a topological space, and given a function `f` from `X` to `AddUnits M` (where `AddUnits M` refers to the additive units in the additive monoid `M`), the function `f` is continuous if and only if both the composition of `AddUnits.val` and `f` is continuous, and the function that takes `x` in `X` to the additive inverse of `f(x)` is continuous. In simpler terms, it connects the continuity of a function into the additive units of a topological additive monoid with the continuity of two related functions.
More concisely: A function from a topological space to the additive units of a topological additive monoid is continuous if and only if the composition of the valuation map and the function, and the function that maps each point to the additive inverse of the image of that point, are both continuous.
|
Units.continuous_iff
theorem Units.continuous_iff :
∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : Monoid M] [inst_2 : TopologicalSpace X]
{f : X → Mˣ}, Continuous f ↔ Continuous (Units.val ∘ f) ∧ Continuous fun x => ↑(f x)⁻¹
This theorem, `Units.continuous_iff`, states that for any type `M` equipped with a topological space and monoid structure, and any type `X` also equipped with a topological space, given a function `f` mapping from `X` to the monoid units of `M`, the function `f` is continuous if and only if two conditions are met: 1) the function that maps every element of `X` to the underlying value of the base monoid via `f` is continuous, and 2) the function that maps every element of `X` to the inverse of the underlying value in the base monoid via `f` is also continuous.
More concisely: A function from a topological space to the units of a monoid equipped with a topology is continuous if and only if the functions mapping each point to the underlying value and its inverse in the monoid are both continuous.
|
AddOpposite.continuous_unop
theorem AddOpposite.continuous_unop : ∀ {M : Type u_1} [inst : TopologicalSpace M], Continuous AddOpposite.unop := by
sorry
This theorem states that for any type `M` endowed with a topological space structure, the operation `AddOpposite.unop` is continuous. In other words, if we have a set `M` where we've defined a notion of "closeness" or "continuity" (i.e., it has a topological space structure), then the process of converting an element from the additive opposite of `M` back to `M` (performed by the function `AddOpposite.unop`) preserves this continuity.
More concisely: For any topological space `M`, the function `AddOpposite.unop : M → M` is continuous.
|
AddUnits.embedding_val_mk
theorem AddUnits.embedding_val_mk :
∀ {M : Type u_3} [inst : SubtractionMonoid M] [inst_1 : TopologicalSpace M],
ContinuousOn Neg.neg {x | IsAddUnit x} → Embedding AddUnits.val
This theorem, named `AddUnits.embedding_val_mk`, states that for every type `M` that is a subtraction monoid and a topological space, if the function that computes the negative or opposite (`Neg.neg`) is continuous at every point of the set of elements that are `AddUnit` in `M`, then the function that gets the underlying value from the base `AddMonoid` (`AddUnits.val`) is an embedding. An embedding, in this context, is a function that is injective (it preserves distinctness) and is also a homeomorphism onto its image (it preserves topological structure). This lemma serves as an auxiliary tool for proving that the coercion from `AddUnits M` to `M` is a topological embedding.
More concisely: Given a subtraction monoid and topological space M with continuous negation function on AddUnit elements, the function mapping AddUnits to their underlying values is an embedding.
|
Units.embedding_val_mk'
theorem Units.embedding_val_mk' :
∀ {M : Type u_3} [inst : Monoid M] [inst_1 : TopologicalSpace M] {f : M → M},
ContinuousOn f {x | IsUnit x} → (∀ (u : Mˣ), f ↑u = ↑u⁻¹) → Embedding Units.val
This theorem, called `Units.embedding_val_mk'`, states that for any type `M` that is a `Monoid` and a `TopologicalSpace`, and any function `f` from `M` to `M`, if `f` is continuous on the set of all units in `M` and `f` maps every element of `Mˣ` (the set of units of `M`) to its inverse, then the function `Units.val`, which takes an element of `Mˣ` and returns its underlying value in `M`, is an embedding. An embedding, in this context, is a function that preserves the topological structure, meaning that the topology of the image is the same as the topology of the original set. This theorem is an auxiliary lemma, meant to be used in proving that the coercion from `Mˣ` to `M` is a topological embedding.
More concisely: If a function from a Monoid and TopologicalSpace `M` that maps units to their inverses and is continuous on units preserves the topological structure of `M`, then the function `Units.val` embedding `Mˣ` into `M` is a topological embedding.
|
AddOpposite.continuous_op
theorem AddOpposite.continuous_op : ∀ {M : Type u_1} [inst : TopologicalSpace M], Continuous AddOpposite.op
The theorem `AddOpposite.continuous_op` states that for any type `M` equipped with a topological space structure, the operation `AddOpposite.op` is continuous. In other words, if we consider `M` as a topological space, then the function that takes an element `x` of `M` and produces the additive opposite `AddOpposite.op x` is a continuous function.
More concisely: The additive opposition operation is a continuous function on any topological space.
|
Units.inducing_embedProduct
theorem Units.inducing_embedProduct :
∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Monoid M], Inducing ⇑(Units.embedProduct M)
This theorem states that for any type `M` equipped with a topological structure and a monoid structure, the canonical homomorphism of monoids from the units of `M` (`Mˣ`) into the product of `M` and the opposite of `M` (`M × Mᵐᵒᵖ`) is an inducing function. In the context of topology, an inducing function is one that induces the topology of its range from the topology of its domain. So, the theorem is saying that the topology on the product space `M × Mᵐᵒᵖ` can be obtained from the topology on the space of units of `M` using this canonical homomorphism.
More concisely: The canonical homomorphism from the units of a topological monoid into the product of the monoid and its opposite is a topology-inducing function.
|
AddUnits.embedding_val_mk'
theorem AddUnits.embedding_val_mk' :
∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : TopologicalSpace M] {f : M → M},
ContinuousOn f {x | IsAddUnit x} → (∀ (u : AddUnits M), f ↑u = ↑(-u)) → Embedding AddUnits.val
This theorem, titled `AddUnits.embedding_val_mk'`, states that, for any type `M` which has an addition monoid structure and a topology, and any function `f` from `M` to `M` that is continuous on the set of elements in `M` which are addUnits, if for every addUnit `u` in `M`, `f` maps the coercion of `u` to the negative of the coercion of `u`, then the function that extracts the underlying value from an addUnit in `M` is an embedding. In simpler terms, under these conditions, the function `AddUnits.val` preserves the structure of the topological space and is injective.
More concisely: Given a type `M` with an addition monoid structure and a topology, if a continuous function `f` from `M` to `M` maps additive units to their negatives, then the function that extracts underlying values from additive units is an embedding.
|
Units.embedding_val_mk
theorem Units.embedding_val_mk :
∀ {M : Type u_3} [inst : DivisionMonoid M] [inst_1 : TopologicalSpace M],
ContinuousOn Inv.inv {x | IsUnit x} → Embedding Units.val
This theorem states that for any type `M`, which is equipped with both a `DivisionMonoid` structure and a `TopologicalSpace` structure, if the inversion function is continuous on all unit elements of `M` (that is, all elements of `M` that have a two-sided inverse), then the function that maps each unit element to its underlying value in the base `Monoid` is an embedding. In other words, this function is both injective (distinct elements in the domain map to distinct elements in the codomain) and continuous, and the inverse function (which exists due to injectiveness) from the image set to the domain set is also continuous. This theorem can be used as a helper lemma while proving that certain coercion functions in the context of topological monoids are topological embeddings.
More concisely: Given a type `M` with both `DivisionMonoid` and `TopologicalSpace` structures, if the inversion function on unit elements is continuous, then the function mapping unit elements to their underlying monoid values is a continuous embedding.
|
MulOpposite.continuous_op
theorem MulOpposite.continuous_op : ∀ {M : Type u_1} [inst : TopologicalSpace M], Continuous MulOpposite.op
The theorem `MulOpposite.continuous_op` states that for any type `M` equipped with a topological space structure, the operation `MulOpposite.op` is continuous. The operation `MulOpposite.op` takes an element from type `M` and represents it as an element of `MulOpposite M`, a type which carries the 'opposite' multiplication structure. The continuity of this operation is stated in terms of the topology on `M` and the induced topology on `MulOpposite M`.
More concisely: The operation `MulOpposite.op` mapping elements from a topological space `M` to `MulOpposite M`, which represents their opposites with respect to a multiplication structure, is a continuous function with respect to the given topology on `M` and the induced topology on `MulOpposite M`.
|
MulOpposite.continuous_unop
theorem MulOpposite.continuous_unop : ∀ {M : Type u_1} [inst : TopologicalSpace M], Continuous MulOpposite.unop := by
sorry
The theorem `MulOpposite.continuous_unop` states that for any type `M` which has a topological space structure, the function `MulOpposite.unop` is continuous. The function `MulOpposite.unop` takes an element from the multiplicative opposite (`MulOpposite`) of `M` and returns an element of `M`. In the context of topology, a function is said to be continuous if the preimage of any open set is also an open set. Thus, in this case, for any open set in `M`, the preimage under `MulOpposite.unop` is an open set in `Mᵐᵒᵖ`.
More concisely: The function `MulOpposite.unop` from the multiplicative opposite of a topological space `M` to `M` is continuous.
|