OrderEmbedding.wellFoundedLT
theorem OrderEmbedding.wellFoundedLT :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β],
α ↪o β → ∀ [inst_2 : WellFoundedLT β], WellFoundedLT α
The theorem `OrderEmbedding.wellFoundedLT` states that for any two types `α` and `β` with preorders defined on them, if `α` embeds into `β` (denoted as `α ↪o β`), and if `β` has a well-founded relation `<`, then `α` also has a well-founded relation `<`. In other words, a preorder which can be embedded into a well-founded preorder is itself well-founded.
More concisely: If `α` embeds into a well-founded preorder `β`, then `α` has a well-founded preorder.
|
OrderHomClass.mono
theorem OrderHomClass.mono :
∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : FunLike F α β]
[inst_3 : OrderHomClass F α β] (f : F), Monotone ⇑f
The theorem `OrderHomClass.mono` states that for any types `F`, `α`, and `β`, given that `α` and `β` are preordered, `F` is a function-like from `α` to `β`, and `F` is a type of less-than-or-equal-to preserving morphisms, then any function `f` of type `F` is monotone. In other words, if `a ≤ b` in the preorder `α`, then `f(a) ≤ f(b)` in the preorder `β`.
More concisely: If `F` is a function-like from a preordered type `α` to a preordered type `β`, and `F` preserves the preorder relation, then `F` is a monotone function.
|
OrderIso.map_bot
theorem OrderIso.map_bot :
∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : PartialOrder β] [inst_2 : OrderBot α] [inst_3 : OrderBot β]
(f : α ≃o β), f ⊥ = ⊥
This theorem states that for any two types `α` and `β` with a lower bound (i.e., they have instances of the `OrderBot` typeclass) and a partial order (i.e., they have an instance of the `PartialOrder` typeclass), if there is an order isomorphism `f` between `α` and `β` (denoted `f : α ≃o β`), then the image of the least element of `α` under `f` is the least element of `β`. In simpler terms, the order isomorphism maps the smallest element of the first set to the smallest element of the second set.
More concisely: Given types `α` and `β` with lower bounds and partial orders, an order isomorphism `f : α ≃o β` implies `f (least α) = least β`.
|
OrderEmbedding.wellFoundedGT
theorem OrderEmbedding.wellFoundedGT :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β],
α ↪o β → ∀ [inst_2 : WellFoundedGT β], WellFoundedGT α
The theorem `OrderEmbedding.wellFoundedGT` states that for any two types `α` and `β` that are preorders, if `α` is order-embedded into `β` (denoted as `α ↪o β`) and `(· > ·)` is a well-founded relation in `β`, then `(· > ·)` is also a well-founded relation in `α`. In other words, if a preordered set can be embedded into another preordered set where the "greater than" relation is well-founded, then the "greater than" relation is also well-founded in the original set.
More concisely: If `α` is order-embedded into a well-founded preordered set `β`, then the relation `(· > ·)` on `α` is also well-founded.
|
Mathlib.Order.Hom.Basic._auxLemma.12
theorem Mathlib.Order.Hom.Basic._auxLemma.12 :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β) {a b : α},
(f a < f b) = (a < b)
This theorem, named `Mathlib.Order.Hom.Basic._auxLemma.12`, asserts that for any two types `α` and `β` that are both preordered, and given an order-embedding function `f` from `α` to `β`, and any two elements `a` and `b` of `α`, the inequality `f(a) < f(b)` holds if and only if `a < b` holds. This theorem essentially says that the order-embedding function `f` preserves the strict less-than order of the elements from `α`.
More concisely: For any preordered types `α` and `β`, and order-embedding `f` from `α` to `β`, if `a < b` in `α`, then `f(a) < f(b)` in `β`.
|
OrderIso.map_sup
theorem OrderIso.map_sup :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] (f : α ≃o β) (x y : α),
f (x ⊔ y) = f x ⊔ f y
This theorem states that for any two types `α` and `β` that are both semilattices with a supremum operation (denoted by `⊔`), any order preserving isomorphism `f` between `α` and `β` preserves the supremum operation. That is, applying `f` to the supremum of `x` and `y` (where `x` and `y` are elements of `α`) is the same as taking the supremum of `f(x)` and `f(y)` (where `f(x)` and `f(y)` are elements of `β`).
More concisely: For any order preserving isomorphism between two semilattices with supremum operation, the image of the supremum of two elements under the isomorphism is equal to the supremum of their images.
|
Codisjoint.map_orderIso
theorem Codisjoint.map_orderIso :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderTop α] [inst_2 : SemilatticeSup β]
[inst_3 : OrderTop β] {a b : α} (f : α ≃o β), Codisjoint a b → Codisjoint (f a) (f b)
The theorem `Codisjoint.map_orderIso` states that for any two elements `a` and `b` in a semilattice `α` with a top element, and a order isomorphism `f` from `α` to another semilattice `β` with a top element, if `a` and `b` are codisjoint in `α` (i.e., for any element `x` in `α`, if `a` and `b` are both less than or equal to `x`, then the top element of `α` is less than or equal to `x`), then the images of `a` and `b` under `f` are also codisjoint in `β`. This means that the property of being codisjoint is preserved under order isomorphisms.
More concisely: If `a` and `b` are codisjoint elements in a semilattice `α` with a top element, and `f` is an order isomorphism from `α` to another semilattice `β` with a top element, then the images `f(a)` and `f(b)` are codisjoint in `β`.
|
OrderHom.monotone
theorem OrderHom.monotone :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), Monotone ⇑f
This theorem states that for any two types `α` and `β` with preorder structures, any order-preserving function `f` from `α` to `β` is necessarily monotone. In other words, if `a` and `b` are elements of `α` such that `a` is less than or equal to `b`, then the image of `a` under `f` is less than or equal to the image of `b` under `f`.
More concisely: For any type `α` and `β` with preorders, and any order-preserving function `f` from `α` to `β`, if `a ≤ b` in `α`, then `f(a) ≤ f(b)` in `β`.
|
OrderIsoClass.map_le_map_iff
theorem OrderIsoClass.map_le_map_iff :
∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : LE α] [inst_1 : LE β] [inst_2 : EquivLike F α β]
[self : OrderIsoClass F α β] (f : F) {a b : α}, f a ≤ f b ↔ a ≤ b
This theorem states that for an order isomorphism, the ordering of mapped elements is preserved. More specifically, if you have any type `F` that is an order isomorphism from `α` to `β`, and any two elements `a` and `b` from `α`, then `a` is less than or equal to `b` if and only if the mapped element `f a` is less than or equal to `f b`. So, for any such order isomorphism `f`, the ordering `≤` is maintained between `α` and `β`.
More concisely: For any order isomorphism between types `α` and `β`, if `a ≤ b` in `α`, then `f(a) ≤ f(b)` in `β`.
|
Mathlib.Order.Hom.Basic._auxLemma.11
theorem Mathlib.Order.Hom.Basic._auxLemma.11 :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β) {a b : α},
(f a ≤ f b) = (a ≤ b)
This theorem, named `Mathlib.Order.Hom.Basic._auxLemma.11`, states that for any two types `α` and `β` that have a Preorder relationship, and for any order-embedding `f` from `α` to `β`, if `a` and `b` are elements of type `α`, then `f(a)` is less than or equal to `f(b)` if and only if `a` is less than or equal to `b`. This basically asserts that the order-embedding `f` preserves the order between the elements of `α`.
More concisely: For any preordered types `α` and `β`, and order-embedding `f` from `α` to `β`, `a ≤ b` in `α` if and only if `f(a) ≤ f(b)` in `β`.
|
OrderEmbedding.le_iff_le
theorem OrderEmbedding.le_iff_le :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β) {a b : α},
f a ≤ f b ↔ a ≤ b
This theorem states that for any two types `α` and `β` that are both preordered, and for any order embedding `f` from `α` to `β`, `f(a)` is less than or equal to `f(b)` if and only if `a` is less than or equal to `b`. This theorem essentially validates that the order embedding `f` correctly preserves the order from `α` to `β`.
More concisely: For any preordered types `α` and `β` and order embedding `f` from `α` to `β`, `f(a) ≤ f(b)` if and only if `a ≤ b` for all `a, b` in `α`.
|
OrderIso.apply_symm_apply
theorem OrderIso.apply_symm_apply :
∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) (x : β), e (e.symm x) = x
The theorem `OrderIso.apply_symm_apply` states that for any types `α` and `β` with a less-than-or-equal-to order (`LE`), given an order isomorphism `e` from `α` to `β` and any element `x` of `β`, applying `e` to the result of applying the inverse of `e` (i.e., `OrderIso.symm e`) to `x` gets us back to the original element `x`. In mathematical terms, it states that if we have an ordered isomorphism between two ordered sets, then this isomorphism is a bijection, meaning that we can go from `β` to `α` using the inverse and then back to `β` using the original isomorphism without changing the original element.
More concisely: Given an order isomorphism between two ordered sets, the composition of the isomorphism with its symmetric inverse is the identity function.
|
OrderIso.ext
theorem OrderIso.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] {f g : α ≃o β}, ⇑f = ⇑g → f = g
This theorem, named "OrderIso.ext", states that for any two types α and β, both equipped with a less-than-or-equal-to relation (LE), if we have two order isomorphisms f and g from α to β, then if the application of f and g produces the same result, then f and g themselves are equal. In other words, this theorem is asserting the uniqueness of order isomorphisms; if two order isomorphisms behave the same way, they're the same isomorphism.
More concisely: If α and β are types equipped with a LE relation, and f and g are order isomorphisms from α to β with f(x) = g(x) for all x in α, then f = g.
|
OrderEmbedding.monotone
theorem OrderEmbedding.monotone :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β), Monotone ⇑f
The theorem `OrderEmbedding.monotone` states that for any two types `α` and `β` with a preorder relation, any order-embedding function `f` from `α` to `β` is monotone. In other words, if `α` and `β` are preordered sets, and `f` is a function that preserves the order from `α` to `β`, then for any two elements `a` and `b` in `α` where `a` is less than or equal to `b`, the image of `a` under `f` is less than or equal to the image of `b` under `f`.
More concisely: If `f` is an order-embedding function from preordered sets `(α, ≤α)` to `(β, ≤β)`, then for all `a ≤ b` in `α`, we have `f(a) ≤ f(b)` in `β`.
|
OrderEmbedding.wellFounded
theorem OrderEmbedding.wellFounded :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β],
α ↪o β → (WellFounded fun x x_1 => x < x_1) → WellFounded fun x x_1 => x < x_1
The theorem `OrderEmbedding.wellFounded` states that for any two types `α` and `β` with a pre-ordering, if there exists an order-preserving embedding from `α` to `β` and if `α` is well-founded (i.e., there are no infinitely descending sequences in `α`), then `β` is also well-founded. In other words, the well-foundedness property for a relation is preserved under order-preserving embeddings.
More concisely: If `α` is a well-founded type with a pre-order and there exists an order-preserving embedding from `α` to `β`, then `β` is also well-founded.
|
OrderHom.monotone'
theorem OrderHom.monotone' :
∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] (self : α →o β), Monotone self.toFun := by
sorry
The theorem `OrderHom.monotone'` states that for any two types `α` and `β` that are both preordered, the underlying function of an order-preserving function (`OrderHom`) from `α` to `β` is monotone. In other words, if `α` and `β` are types with a preorder, and `self` is a function from `α` to `β` that preserves order, then for any two elements `a` and `b` in `α` such that `a` is less than or equal to `b`, the value of the function `self` at `a` is less than or equal to the value of the function `self` at `b`.
More concisely: For any order-preserving function `f` from a preordered type `(α, ≤α)` to a preordered type `(β, ≤β)`, if `a ≤ b` in `α`, then `f a ≤ f b` in `β`.
|
OrderEmbedding.lt_iff_lt
theorem OrderEmbedding.lt_iff_lt :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β) {a b : α},
f a < f b ↔ a < b
The theorem `OrderEmbedding.lt_iff_lt` states that for any two types `α` and `β` that are both preordered, and any order-embedding function `f` from `α` to `β`, the images `f a` and `f b` of any two elements `a` and `b` of `α` under `f` satisfy `f a < f b` if and only if `a < b`. In other words, the order-embedding function preserves the order of the elements from `α` into `β`.
More concisely: For any preordered types `α` and `β` and order-embedding function `f` from `α` to `β`, `a < b` in `α` implies `f a < f b` in `β`.
|
OrderEmbedding.strictMono
theorem OrderEmbedding.strictMono :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β), StrictMono ⇑f
The theorem `OrderEmbedding.strictMono` states that for any two types `α` and `β`, both having a preorder (a binary relation that is reflexive and transitive), any order-embedding function `f` from `α` to `β` is strictly monotone. Here, an order-embedding function is a function that preserves the order of the elements. Strict monotonicity means that if `a` is less than `b` in the type `α`, then `f(a)` is less than `f(b)` in the type `β`.
More concisely: Given types `α` and `β` with preorders, any order-embedding function `f` from `α` to `β` is a strictly increasing function.
|
OrderIso.surjective
theorem OrderIso.surjective :
∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β), Function.Surjective ⇑e
The theorem `OrderIso.surjective` states that for any two types `α` and `β` that have an order relation (represented by `LE α` and `LE β` respectively), if there is an order isomorphism `e` between `α` and `β` (denoted by `α ≃o β`), then the function represented by `e` (obtained by applying the coercion to function, `⇑e`) is surjective. In terms of mathematics, this means that for every element `b` from `β`, there exists an element `a` from `α` such that `b` is the image of `a` under the function represented by `e`. This theorem essentially asserts that every order isomorphism is a surjective function.
More concisely: For any order isomorphic types `α` and `β`, the order isomorphism between them induces a surjective function from `α` to `β`.
|
OrderIso.complementedLattice_iff
theorem OrderIso.complementedLattice_iff :
∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
[inst_3 : BoundedOrder β], α ≃o β → (ComplementedLattice α ↔ ComplementedLattice β)
The theorem `OrderIso.complementedLattice_iff` states that for any two types `α` and `β` with Lattice and BoundedOrder structures, if `α` is order-isomorphic to `β` (denoted as `α ≃o β`), then `α` is a complemented lattice if and only if `β` is a complemented lattice. In other words, the property of being a complemented lattice is preserved under order isomorphism. A complemented lattice is a lattice in which every element has a complement, i.e., for any element, there is another element such that their meet and join are the lattice's bottom and top elements, respectively.
More concisely: If two types equipped with Lattice and BoundedOrder structures are order-isomorphic, then they have the same property of being complemented lattices.
|
OrderIso.le_symm_apply
theorem OrderIso.le_symm_apply :
∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) {x : α} {y : β},
x ≤ e.symm y ↔ e x ≤ y
This theorem states that for any two types `α` and `β` that have a less than or equal to (`≤`) relationship, and for any order isomorphism `e` between `α` and `β`, the inequality `x ≤ (OrderIso.symm e) y` holds if and only if `e x ≤ y` holds, where `x` is an element of `α` and `y` is an element of `β`. In other words, applying the inverse of the order isomorphism to `y` and comparing it with `x` in `α` is equivalent to transforming `x` into `β` using the order isomorphism `e` and comparing it with `y` in `β`.
More concisely: For any order isomorphism between types `α` and `β`, and for all `x` in `α` and `y` in `β`, `x ≤ y` if and only if `e x ≤ y` or `y ≤ e x`, where `e` is the order isomorphism.
|
OrderHom.ext
theorem OrderHom.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f g : α →o β), ⇑f = ⇑g → f = g := by
sorry
This theorem states that for any two order-preserving functions `f` and `g` from a preorder `α` to a preorder `β`, if the functions `f` and `g` are equal when applied to every element (denoted by `⇑f = ⇑g`), then the functions `f` and `g` themselves are equal (`f = g`). In other words, two order-preserving functions are considered identical if and only if they return the same result for every input from the preordered set.
More concisely: If `α` is a preorder and `f` and `g` are order-preserving functions from `α` to a preorder `β` with `⇑f = ⇑g`, then `f = g`.
|
OrderHom.mono
theorem OrderHom.mono :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), Monotone ⇑f
This theorem, `OrderHom.mono`, states that for any two types `α` and `β` that are equipped with a preorder structure, any order-preserving function (an `OrderHom`) `f` from `α` to `β` is monotone. In other words, if `a ≤ b` in `α` then `f(a) ≤ f(b)` in `β`, where `a` and `b` are elements of type `α`, and `f` is a function from `α` to `β`.
More concisely: For any type-preserving function between preordered types, if it respects the preorder relation then it is monotone.
|
OrderIso.symm_apply_apply
theorem OrderIso.symm_apply_apply :
∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) (x : α), e.symm (e x) = x
This theorem states that for any types `α` and `β` that have an order relation (denoted by `LE α` and `LE β`), given an order isomorphism `e` from `α` to `β` and any element `x` of `α`, applying `e` to `x` and then applying the inverse of `e` (denoted by `OrderIso.symm e`) to the result will bring us back to the original element `x`. In other words, the inverse of an order isomorphism undoes the action of the isomorphism. This is analogous to the mathematical concept where the inverse of a function undoes the action of the function itself.
More concisely: For any order isomorphisms `e: α → β` between ordered types `α` and `β`, `e (x) = OrderIso.symm e (e x)` for all `x` in `α`.
|
OrderIso.bijective
theorem OrderIso.bijective :
∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β), Function.Bijective ⇑e
This theorem states that for any two types `α` and `β` that have a less than or equal to order (`LE`), if there exists an order isomorphism (`≃o`) `e` between `α` and `β`, then the function represented by `e` (denoted by `⇑e` in Lean) is bijective. In mathematical terms, an order isomorphism between two ordered sets is a bijective function that preserves the ordering, meaning if `x ≤ y` in `α`, then `f(x) ≤ f(y)` in `β`, and vice versa.
More concisely: If `α` and `β` are ordered types with a less than or equal to order relation (`LE`) and there exists an order isomorphism (`≃o`) between them, then the function `f : α → β` represented by `e : α ≃o β` is a bidirectional, order-preserving bijection.
|
Mathlib.Order.Hom.Basic._auxLemma.1
theorem Mathlib.Order.Hom.Basic._auxLemma.1 :
∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : LE α] [inst_1 : LE β] [inst_2 : EquivLike F α β]
[self : OrderIsoClass F α β] (f : F) {a b : α}, (f a ≤ f b) = (a ≤ b)
This theorem, named `_auxLemma.1` from `Mathlib.Order.Hom.Basic`, states that for any types `F`, `α`, and `β`, with `α` and `β` being types with less-than-or-equal-to (`≤`) relations, and `F` being a type that behaves like an equivalence between `α` and `β`, the following holds: If `F` also represents an order-isomorphism class (denoted by `OrderIsoClass F α β`), then for any function `f` of type `F` and any two elements `a` and `b` of type `α`, the statement "`f a` is less than or equal to `f b`" is equivalent to the statement "`a` is less than or equal to `b`". In other words, the order-isomorphism preserves the order of elements.
More concisely: For any type `F` behaving like an equivalence between types `α` and `β` with less-than-or-equal-to relations, if `F` is an order isomorphism, then `x ≤ y` in `α` if and only if `F x ≤ F y` in `β`.
|
OrderIso.injective
theorem OrderIso.injective :
∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β), Function.Injective ⇑e
The theorem `OrderIso.injective` states that for any two types `α` and `β`, if `α` and `β` are equipped with `≤` order relations (denoted by `inst : LE α` and `inst_1 : LE β` respectively) and there exists an order isomorphism `e : α ≃o β` between them, then the function represented by `e` (denoted by `⇑e`) is injective. In other words, if `e` maps two elements in `α` to the same element in `β`, then those two elements in `α` were the same.
More concisely: If `α` and `β` are ordered types with an order isomorphism between them, then the order isomorphism is an injection.
|
OrderIso.coe_toOrderEmbedding
theorem OrderIso.coe_toOrderEmbedding :
∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β), ⇑e.toOrderEmbedding = ⇑e
This theorem states that for any two types `α` and `β` which have defined less than or equal to operations (`LE`), any order isomorphism `e` from `α` to `β` remains unchanged when reinterpreted as an order embedding. In other words, the function `OrderIso.toOrderEmbedding` does not modify the behavior of the order isomorphism when converting it to an order embedding. It simply changes the way it is viewed or used. This is expressed by the equality `⇑(OrderIso.toOrderEmbedding e) = ⇑e`, where `⇑` is the coercion function that applies the isomorphism or embedding to an element of `α`.
More concisely: The order isomorphism between types `α` and `β` remains the same when converted from an order isomorphism to an order embedding using `OrderIso.toOrderEmbedding`.
|
OrderIso.map_inf
theorem OrderIso.map_inf :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] (f : α ≃o β) (x y : α),
f (x ⊓ y) = f x ⊓ f y
This theorem states that for any two types `α` and `β`, given that they are both semilattices with respect to the infimum operation (a binary operation which for any two elements returns the greatest element that is less than or equal to both), an order isomorphism `f` from `α` to `β` preserves the infimum operation. That is, applying `f` to the infimum of `x` and `y` (denoted as `x ⊓ y`) results in the same output as the infimum of `f(x)` and `f(y)` (`f x ⊓ f y`). This is a statement about the structure-preserving property of order isomorphisms in the context of semilattices.
More concisely: Given two semilattices `α` and `β` and an order isomorphism `f` from `α` to `β`, for all `x, y ∈ α`, we have `f (x ⊓ y) = f(x) ⊓ f(y)`.
|
OrderIso.symm_apply_le
theorem OrderIso.symm_apply_le :
∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) {x : α} {y : β},
e.symm y ≤ x ↔ y ≤ e x
This theorem states that for any types `α` and `β` equipped with a less-than-or-equal-to (`≤`) relation, and given an order isomorphism `e` between `α` and `β`, the less-than-or-equal-to (`≤`) relation between the image of a variable `y` under the inverse of the isomorphism `(OrderIso.symm e) y` and a variable `x` in `α`, is equivalent to the relation of `y` being less than or equal to the image of `x` under the isomorphism `e x`. In mathematical terms, this is saying that `(OrderIso.symm e) y ≤ x` if and only if `y ≤ e x` for all `x` in `α` and `y` in `β`.
More concisely: For any order isomorphisms between types `α` and `β` and for all `x` in `α` and `y` in `β`, `(OrderIso.symm e) y ≤ x` if and only if `y ≤ e x`.
|
OrderIso.map_top
theorem OrderIso.map_top :
∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : PartialOrder β] [inst_2 : OrderTop α] [inst_3 : OrderTop β]
(f : α ≃o β), f ⊤ = ⊤
This theorem, `OrderIso.map_top`, states that for any two types `α` and `β` where `α` is an ordered type having a top element, `β` is a partially ordered type also having a top element, and there is an order isomorphism `f` from `α` to `β`, applying the order isomorphism `f` to the top element of `α` gives the top element of `β`. In more mathematical terms, if `⊤` is the top element in `α`, then `f(⊤) = ⊤` in `β`.
More concisely: For any ordered type `α` with top element `⊤` and a order isomorphism `f` to a partially ordered type `β` with top element `⊤`, `f(⊤) = ⊤`.
|
OrderIso.lt_iff_lt
theorem OrderIso.lt_iff_lt :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) {x y : α},
e x < e y ↔ x < y
This theorem states that for any two types `α` and `β` that have a preorder (a binary relation that is reflexive and transitive), if there is an order-preserving isomorphism `e` from `α` to `β`, then for any two elements `x` and `y` in `α`, `x` is less than `y` if and only if `e(x)` is less than `e(y)`. In other words, the order-preserving isomorphism preserves the less-than relation.
More concisely: Given types `α` and `β` with a preorder, an order-preserving isomorphism `e` from `α` to `β` implies that `x ≤ y` in `α` if and only if `e(x) ≤ e(y)` in `β`.
|
OrderIso.strictMono
theorem OrderIso.strictMono :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β), StrictMono ⇑e
The theorem `OrderIso.strictMono` states that for any two types `α` and `β`, each equipped with a preorder relation, if there is an order isomorphism `e` between `α` and `β`, then the function represented by `e` is strictly monotone. In other words, for any `a` and `b` of type `α`, if `a < b`, then `e(a) < e(b)`. This asserts a particular property of order isomorphisms: they preserve the strict order of elements in the original preorder.
More concisely: If `e` is an order isomorphism between preordered types `α` and `β`, then `e(a) < e(b)` whenever `a < b` in `α`.
|
Mathlib.Order.Hom.Basic._auxLemma.13
theorem Mathlib.Order.Hom.Basic._auxLemma.13 :
∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β], (fun f => ⇑f) = DFunLike.coe
The theorem `Mathlib.Order.Hom.Basic._auxLemma.13` states that for any type `F` in a certain universe `u_1`, any type `α` in a certain universe `u_2`, and any type function `β` which maps elements of `α` to types in a certain universe `u_3`, if there exists a structure `i` of the typeclass `DFunLike F α β`, then the function which maps each element `f` of the type `F` to its coercion function `⇑f` is exactly the `DFunLike.coe` function. In other words, the coercion operator `⇑` and `DFunLike.coe` act the same way under these conditions.
More concisely: If `F` is a type in universe `u_1`, `α` is a type in universe `u_2`, and `β` is a type function mapping elements of `α` to types in universe `u_3`, then the function mapping each `f` in `F` to its coercion `⇑f` is equal to the `DFunLike.coe` function for the typeclass `DFunLike F α β`, i.e., `⇑f = DFunLike.coe f`.
|
OrderIso.symm_symm
theorem OrderIso.symm_symm :
∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β), e.symm.symm = e
The theorem `OrderIso.symm_symm` states that for any two types `α` and `β`, both equipped with an order relation (`LE`), given an order isomorphism `e` from `α` to `β`, the double application of the operation `OrderIso.symm` (which takes the inverse of an order isomorphism) to `e` gives back `e`. Essentially, this theorem ensures that taking the inverse twice gives you the original order isomorphism.
More concisely: For any order isomorphism `e` between types `α` and `β` equipped with order relations `LEα` and `LEβ` respectively, we have `OrderIso.symm (OrderIso.symm e) = e`.
|
OrderIso.le_iff_le
theorem OrderIso.le_iff_le :
∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) {x y : α}, e x ≤ e y ↔ x ≤ y
This theorem states that for any two types `α` and `β` with a less than or equal to (`≤`) ordering, if there exists an order isomorphism (`≃o`) `e` from `α` to `β`, then for any two elements `x` and `y` of type `α`, `x` is less than or equal to `y` if and only if `e(x)` is less than or equal to `e(y)`. Basically, the order isomorphism `e` preserves the order of elements when mapping from `α` to `β`.
More concisely: For any order isomorphism `e` between types `α` and `β`, `x ≤ y` in `α` if and only if `e(x) ≤ e(y)` in `β`.
|
Disjoint.map_orderIso
theorem Disjoint.map_orderIso :
∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderBot α] [inst_2 : SemilatticeInf β]
[inst_3 : OrderBot β] {a b : α} (f : α ≃o β), Disjoint a b → Disjoint (f a) (f b)
The theorem `Disjoint.map_orderIso` states that for any two elements `a` and `b` in a semilattice with a bottom element (which is a type of partial order), if `a` and `b` are disjoint, then their images under any order isomorphism `f` also are disjoint.
Here, `Disjoint a b` means that any element `x` which is less than or equal to both `a` and `b` is also less than or equal to the bottom element (denoted `⊥`). This definition of disjointness generalizes the concept of disjoint sets. An order isomorphism `f` is a bijective function that preserves the order relation, that is, for any two elements `x` and `y`, `x ≤ y` if and only if `f(x) ≤ f(y)`.
More concisely: If `a` and `b` are disjoint elements in a semilattice with a bottom element and `f` is an order isomorphism, then `f(a)` and `f(b)` are also disjoint.
|
OrderIso.monotone
theorem OrderIso.monotone :
∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β), Monotone ⇑e
This theorem states that for any types `α` and `β` with a preorder relation, and for any order isomorphism `e` from `α` to `β`, the function `e` is monotone. In other words, if `a` and `b` are elements of `α` such that `a` is less than or equal to `b`, then the image of `a` under `e` is less than or equal to the image of `b` under `e`. This property holds for all order isomorphisms between preordered sets, which reflect the order structure of one set onto another.
More concisely: For any preordered types `α` and `β` and order isomorphism `e` from `α` to `β`, `e (a ≤ b)` implies `e(a) ≤ e(b)` for all `a, b` in `α`.
|