TopHomClass.map_top
theorem TopHomClass.map_top :
∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : Top α] [inst_1 : Top β] [inst_2 : FunLike F α β]
[self : TopHomClass F α β] (f : F), f ⊤ = ⊤
The theorem `TopHomClass.map_top` states that for any types `F`, `α`, and `β`, where `α` and `β` have a top element (represented by the `Top α` and `Top β` instances), and `F` is a function-like object from `α` to `β` (represented by instance `FunLike F α β`), if `F` belongs to the `TopHomClass` (meaning it is a morphism that respects the top element structure), then applying the function `F` to the top element of `α` will yield the top element of `β`. In other words, a `TopHomClass` morphism preserves the top element under application.
More concisely: If `F` is a function-like object from a type `α` with top element to a type `β` with top element, belonging to the `TopHomClass` of morphisms preserving top elements, then `F` maps the top element of `α` to the top element of `β`.
|
BotHom.ext
theorem BotHom.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : Bot β] {f g : BotHom α β},
(∀ (a : α), f a = g a) → f = g
This theorem states that for any two types, `α` and `β`, both equipped with a bottom element (`Bot`), if two morphisms `f` and `g` from `α` to `β` (i.e., two `BotHom` from `α` to `β`) map every element of `α` to the same element in `β`, then `f` and `g` are essentially the same morphism. In other words, two `BotHom` are equal if they are point-wise equal.
More concisely: Given types `α` and `β` with bottom elements `Botα` and `Botβ`, respectively, and morphisms `f : α → β` and `g : α → β` such that `f (Botα) = g (Botα)`, then `f = g`.
|
TopHom.ext
theorem TopHom.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : Top β] {f g : TopHom α β},
(∀ (a : α), f a = g a) → f = g
This theorem states that for any types `α` and `β` which have a topology (`Top α` and `Top β`), if there are two continuous functions (`TopHom α β`), `f` and `g`, that map elements of `α` to `β`, then if for each element `a` in `α`, `f(a)` equals `g(a)`, it implies that the functions `f` and `g` are equal. In simpler terms, it says that if two continuous functions from one topological space to another always yield the same results for the same inputs, then those two functions are considered to be the same.
More concisely: If `α` and `β` are topological spaces, and `f` and `g` are continuous functions `α → β` with `f(a) = g(a)` for all `a ∈ α`, then `f = g`.
|
BoundedOrderHom.map_bot'
theorem BoundedOrderHom.map_bot' :
∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : BoundedOrder α]
[inst_3 : BoundedOrder β] (self : BoundedOrderHom α β), self.toFun ⊥ = ⊥
This theorem, named `BoundedOrderHom.map_bot'`, states that for any two types `α` and `β` that are preordered and have a bounded order, a bounded order homomorphism from `α` to `β` preserves the bottom element. In simpler terms, when the function (homomorphism) defined in `BoundedOrderHom α β` is applied to the bottom element (the smallest element) of `α`, it produces the bottom element of `β`. The theorem is also known as `map_bot`.
More concisely: Given preordered types `α` and `β` with bounded orders and a bounded order homomorphism `f : α → β`, we have `f (Inf α) = Inf β`.
|
BoundedOrderHom.map_top'
theorem BoundedOrderHom.map_top' :
∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : BoundedOrder α]
[inst_3 : BoundedOrder β] (self : BoundedOrderHom α β), self.toFun ⊤ = ⊤
This theorem states that for any bounded order homomorphism `self` from a given type `α` to another type `β` -- where both types `α` and `β` are equipped with a preorder and a bounded order structure -- the image of the top element of `α` under this homomorphism is the top element of `β`. In other words, this bounded order homomorphism preserves the top element. The preferred name for this theorem is `map_top`.
More concisely: For any bounded order homomorphism from a preordered type to another preordered type, the image of the top element is the top element.
|
BoundedOrderHomClass.map_top
theorem BoundedOrderHomClass.map_top :
∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : LE α] [inst_1 : LE β] [inst_2 : BoundedOrder α]
[inst_3 : BoundedOrder β] [inst_4 : FunLike F α β] [self : BoundedOrderHomClass F α β] (f : F), f ⊤ = ⊤
The theorem `BoundedOrderHomClass.map_top` states that for any types `F`, `α`, and `β`, given that `α` and `β` are both bounded ordered sets, and `F` is a function-like structure from `α` to `β`, if `f` is a instance of a bounded order homomorphism class from `α` to `β`, then the top element of `α` when mapped by `f` results in the top element of `β`. This essentially means that morphisms preserve the top element in the context of bounded ordered sets.
More concisely: For any bounded ordered sets `α` and `β`, and a bounded order homomorphism `f` from `α` to `β`, the map of the top element of `α` under `f` is the top element of `β`.
|
BotHom.map_bot'
theorem BotHom.map_bot' :
∀ {α : Type u_6} {β : Type u_7} [inst : Bot α] [inst_1 : Bot β] (self : BotHom α β), self.toFun ⊥ = ⊥
This theorem, named `BotHom.map_bot'`, states that for any types `α` and `β` that have a bottom element (indicated by the `Bot α` and `Bot β` typeclasses), any function that is a homomorphism of bottom elements, represented by `BotHom α β`, preserves the bottom element. In simpler terms, when the bottom element of α is passed to this function, it will return the bottom element of β. The theorem's preferred name is `map_bot`.
More concisely: For any types `α` and `β` with bottom elements and any `BotHom α β` function, `f (Bot α) = Bot β`.
|
BotHomClass.map_bot
theorem BotHomClass.map_bot :
∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : Bot α] [inst_1 : Bot β] [inst_2 : FunLike F α β]
[self : BotHomClass F α β] (f : F), f ⊥ = ⊥
The theorem `BotHomClass.map_bot` states that for any types `F`, `α`, and `β`, if `α` and `β` have bottom elements (denoted by `Bot`), and `F` is a functional type from `α` to `β` (expressed by `FunLike F α β`), and if `F` also has a `BotHomClass` structure between `α` and `β`, then any function `f` of type `F` preserves the bottom element. In other words, applying the function `f` to the bottom element of `α` gives the bottom element of `β`, which can be written symbolically as `f ⊥ = ⊥`.
More concisely: For any functional type `F` from types `α` and `β` with bottom elements, having a `BotHomClass` structure preserves the bottom element, i.e., `F (Bot α) = Bot β`.
|
BoundedOrderHomClass.map_bot
theorem BoundedOrderHomClass.map_bot :
∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : LE α] [inst_1 : LE β] [inst_2 : BoundedOrder α]
[inst_3 : BoundedOrder β] [inst_4 : FunLike F α β] [self : BoundedOrderHomClass F α β] (f : F), f ⊥ = ⊥
This theorem states that for any morphism `f` of type `F` where `F` is a function-like structure that maps from one type `α` to another type `β`, both of which are bounded orders (meaning they have a least element, often denoted as `⊥`), the mapping of the least element of `α` under the morphism `f` yields the least element of `β`. In other words, morphisms preserve the least element in the order. The theorem is generally referred to as `map_bot`.
More concisely: For any function-like morphism `f` between bounded types `α` and `β`, `f ⊥ = ⊥`.
|
BoundedOrderHom.ext
theorem BoundedOrderHom.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : BoundedOrder α]
[inst_3 : BoundedOrder β] {f g : BoundedOrderHom α β}, (∀ (a : α), f a = g a) → f = g
This theorem states that given two types `α` and `β` which are preordered and have a bounded order, and given two bounded order homomorphisms `f` and `g` from `α` to `β`, if for every element `a` of type `α`, `f(a)` equals `g(a)`, then `f` and `g` must be the same bounded order homomorphism. In other words, it asserts the uniqueness of a bounded order homomorphism under the condition that they map each element in the domain to the same element in the codomain.
More concisely: If two bounded order homomorphisms between preordered types with a bounded order map every element to the same image, then they are equal.
|
TopHom.map_top'
theorem TopHom.map_top' :
∀ {α : Type u_6} {β : Type u_7} [inst : Top α] [inst_1 : Top β] (self : TopHom α β), self.toFun ⊤ = ⊤
This theorem, referred to as `TopHom.map_top'`, states that for any two types `α` and `β` that have a top element (denoted as `⊤`), any homomorphism from `α` to `β` (denoted as `self : TopHom α β`) will preserve the top element. In other words, applying the function `self.toFun` to the top element of `α` will yield the top element of `β`. This property is often referred to as "mapping the top element", hence the alternate name `map_top`.
More concisely: For any topological spaces `α` and `β` with top elements `⊤α` and `⊤β` respectively, and any topology-preserving function `f : α → β` (i.e., a homomorphism in the category of topological spaces), `f(⊤α) = ⊤β`.
|