# mathlib3documentation

order.locally_finite

# Locally finite orders #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines locally finite orders.

A locally finite order is an order for which all bounded intervals are finite. This allows to make sense of `Icc`/`Ico`/`Ioc`/`Ioo` as lists, multisets, or finsets. Further, if the order is bounded above (resp. below), then we can also make sense of the "unbounded" intervals `Ici`/`Ioi` (resp. `Iic`/`Iio`).

Many theorems about these intervals can be found in `data.finset.locally_finite`.

## Examples #

Naturally occurring locally finite orders are `ℕ`, `ℤ`, `ℕ+`, `fin n`, `α × β` the product of two locally finite orders, `α →₀ β` the finitely supported functions to a locally finite order `β`...

## Main declarations #

In a `locally_finite_order`,

• `finset.Icc`: Closed-closed interval as a finset.
• `finset.Ico`: Closed-open interval as a finset.
• `finset.Ioc`: Open-closed interval as a finset.
• `finset.Ioo`: Open-open interval as a finset.
• `finset.uIcc`: Unordered closed interval as a finset.
• `multiset.Icc`: Closed-closed interval as a multiset.
• `multiset.Ico`: Closed-open interval as a multiset.
• `multiset.Ioc`: Open-closed interval as a multiset.
• `multiset.Ioo`: Open-open interval as a multiset.

In a `locally_finite_order_top`,

• `finset.Ici`: Closed-infinite interval as a finset.
• `finset.Ioi`: Open-infinite interval as a finset.
• `multiset.Ici`: Closed-infinite interval as a multiset.
• `multiset.Ioi`: Open-infinite interval as a multiset.

In a `locally_finite_order_bot`,

• `finset.Iic`: Infinite-open interval as a finset.
• `finset.Iio`: Infinite-closed interval as a finset.
• `multiset.Iic`: Infinite-open interval as a multiset.
• `multiset.Iio`: Infinite-closed interval as a multiset.

## Instances #

A `locally_finite_order` instance can be built

• for a subtype of a locally finite order. See `subtype.locally_finite_order`.
• for the product of two locally finite orders. See `prod.locally_finite_order`.
• for any fintype (but not as an instance). See `fintype.to_locally_finite_order`.
• from a definition of `finset.Icc` alone. See `locally_finite_order.of_Icc`.
• by pulling back `locally_finite_order β` through an order embedding `f : α →o β`. See `order_embedding.locally_finite_order`.

Instances for concrete types are proved in their respective files:

• `ℕ` is in `data.nat.interval`
• `ℤ` is in `data.int.interval`
• `ℕ+` is in `data.pnat.interval`
• `fin n` is in `data.fin.interval`
• `finset α` is in `data.finset.interval`
• `Σ i, α i` is in `data.sigma.interval` Along, you will find lemmas about the cardinality of those finite intervals.

## TODO #

Provide the `locally_finite_order` instance for `α ×ₗ β` where `locally_finite_order α` and `fintype β`.

Provide the `locally_finite_order` instance for `α →₀ β` where `β` is locally finite. Provide the `locally_finite_order` instance for `Π₀ i, β i` where all the `β i` are locally finite.

From `linear_order α`, `no_max_order α`, `locally_finite_order α`, we can also define an order isomorphism `α ≃ ℕ` or `α ≃ ℤ`, depending on whether we have `order_bot α` or `no_min_order α` and `nonempty α`. When `order_bot α`, we can match `a : α` to `(Iio a).card`.

We can provide `succ_order α` from `linear_order α` and `locally_finite_order α` using

``````lemma exists_min_greater [linear_order α] [locally_finite_order α] {x ub : α} (hx : x < ub) :
∃ lub, x < lub ∧ ∀ y, x < y → lub ≤ y :=
begin -- very non golfed
have h : (finset.Ioc x ub).nonempty := ⟨ub, finset.mem_Ioc_iff.2 ⟨hx, le_rfl⟩⟩,
use finset.min' (finset.Ioc x ub) h,
split,
{ have := finset.min'_mem _ h,
simp * at * },
rintro y hxy,
obtain hy | hy := le_total y ub,
apply finset.min'_le,
simp * at *,
exact (finset.min'_le _ _ (finset.mem_Ioc_iff.2 ⟨hx, le_rfl⟩)).trans hy,
end
``````

Note that the converse is not true. Consider `{-2^z | z : ℤ} ∪ {2^z | z : ℤ}`. Any element has a successor (and actually a predecessor as well), so it is a `succ_order`, but it's not locally finite as `Icc (-1) 1` is infinite.

@[class]
structure locally_finite_order (α : Type u_1) [preorder α] :
Type u_1

A locally finite order is an order where bounded intervals are finite. When you don't care too much about definitional equality, you can use `locally_finite_order.of_Icc` or `locally_finite_order.of_finite_Icc` to build a locally finite order from just `finset.Icc`.

Instances of this typeclass
Instances of other typeclasses for `locally_finite_order`
@[class]
structure locally_finite_order_top (α : Type u_1) [preorder α] :
Type u_1
• finset_Ioi : α
• finset_Ici : α
• finset_mem_Ici : (a x : α),
• finset_mem_Ioi : (a x : α),

A locally finite order top is an order where all intervals bounded above are finite. This is slightly weaker than `locally_finite_order` + `order_top` as it allows empty types.

Instances of this typeclass
Instances of other typeclasses for `locally_finite_order_top`
@[class]
structure locally_finite_order_bot (α : Type u_1) [preorder α] :
Type u_1
• finset_Iio : α
• finset_Iic : α
• finset_mem_Iic : (a x : α),
• finset_mem_Iio : (a x : α),

A locally finite order bot is an order where all intervals bounded below are finite. This is slightly weaker than `locally_finite_order` + `order_bot` as it allows empty types.

Instances of this typeclass
Instances of other typeclasses for `locally_finite_order_bot`
def locally_finite_order.of_Icc' (α : Type u_1) [preorder α] (finset_Icc : α α ) (mem_Icc : (a b x : α), x finset_Icc a b a x x b) :

A constructor from a definition of `finset.Icc` alone, the other ones being derived by removing the ends. As opposed to `locally_finite_order.of_Icc`, this one requires `decidable_rel (≤)` but only `preorder`.

Equations
def locally_finite_order.of_Icc (α : Type u_1) [decidable_eq α] (finset_Icc : α α ) (mem_Icc : (a b x : α), x finset_Icc a b a x x b) :

A constructor from a definition of `finset.Icc` alone, the other ones being derived by removing the ends. As opposed to `locally_finite_order.of_Icc`, this one requires `partial_order` but only `decidable_eq`.

Equations
def locally_finite_order_top.of_Ici' (α : Type u_1) [preorder α] (finset_Ici : α ) (mem_Ici : (a x : α), x finset_Ici a a x) :

A constructor from a definition of `finset.Iic` alone, the other ones being derived by removing the ends. As opposed to `locally_finite_order_top.of_Ici`, this one requires `decidable_rel (≤)` but only `preorder`.

Equations
def locally_finite_order_top.of_Ici (α : Type u_1) [decidable_eq α] (finset_Ici : α ) (mem_Ici : (a x : α), x finset_Ici a a x) :

A constructor from a definition of `finset.Iic` alone, the other ones being derived by removing the ends. As opposed to `locally_finite_order_top.of_Ici'`, this one requires `partial_order` but only `decidable_eq`.

Equations
def locally_finite_order_bot.of_Iic' (α : Type u_1) [preorder α] (finset_Iic : α ) (mem_Iic : (a x : α), x finset_Iic a x a) :

A constructor from a definition of `finset.Iic` alone, the other ones being derived by removing the ends. As opposed to `locally_finite_order.of_Icc`, this one requires `decidable_rel (≤)` but only `preorder`.

Equations
def locally_finite_order_top.of_Iic (α : Type u_1) [decidable_eq α] (finset_Iic : α ) (mem_Iic : (a x : α), x finset_Iic a x a) :

A constructor from a definition of `finset.Iic` alone, the other ones being derived by removing the ends. As opposed to `locally_finite_order_top.of_Ici'`, this one requires `partial_order` but only `decidable_eq`.

Equations
@[protected, reducible]

An empty type is locally finite.

This is not an instance as it would not be defeq to more specific instances.

Equations
@[protected, reducible]

An empty type is locally finite.

This is not an instance as it would not be defeq to more specific instances.

Equations
@[protected, reducible]

An empty type is locally finite.

This is not an instance as it would not be defeq to more specific instances.

Equations

### Intervals as finsets #

def finset.Icc {α : Type u_1} [preorder α] (a b : α) :

The finset of elements `x` such that `a ≤ x` and `x ≤ b`. Basically `set.Icc a b` as a finset.

Equations
def finset.Ico {α : Type u_1} [preorder α] (a b : α) :

The finset of elements `x` such that `a ≤ x` and `x < b`. Basically `set.Ico a b` as a finset.

Equations
def finset.Ioc {α : Type u_1} [preorder α] (a b : α) :

The finset of elements `x` such that `a < x` and `x ≤ b`. Basically `set.Ioc a b` as a finset.

Equations
def finset.Ioo {α : Type u_1} [preorder α] (a b : α) :

The finset of elements `x` such that `a < x` and `x < b`. Basically `set.Ioo a b` as a finset.

Equations
@[simp]
theorem finset.mem_Icc {α : Type u_1} [preorder α] {a b x : α} :
x b a x x b
@[simp]
theorem finset.mem_Ico {α : Type u_1} [preorder α] {a b x : α} :
x b a x x < b
@[simp]
theorem finset.mem_Ioc {α : Type u_1} [preorder α] {a b x : α} :
x b a < x x b
@[simp]
theorem finset.mem_Ioo {α : Type u_1} [preorder α] {a b x : α} :
x b a < x x < b
@[simp, norm_cast]
theorem finset.coe_Icc {α : Type u_1} [preorder α] (a b : α) :
b) = b
@[simp, norm_cast]
theorem finset.coe_Ico {α : Type u_1} [preorder α] (a b : α) :
b) = b
@[simp, norm_cast]
theorem finset.coe_Ioc {α : Type u_1} [preorder α] (a b : α) :
b) = b
@[simp, norm_cast]
theorem finset.coe_Ioo {α : Type u_1} [preorder α] (a b : α) :
b) = b
def finset.Ici {α : Type u_1} [preorder α] (a : α) :

The finset of elements `x` such that `a ≤ x`. Basically `set.Ici a` as a finset.

Equations
def finset.Ioi {α : Type u_1} [preorder α] (a : α) :

The finset of elements `x` such that `a < x`. Basically `set.Ioi a` as a finset.

Equations
@[simp]
theorem finset.mem_Ici {α : Type u_1} [preorder α] {a x : α} :
x a x
@[simp]
theorem finset.mem_Ioi {α : Type u_1} [preorder α] {a x : α} :
x a < x
@[simp, norm_cast]
theorem finset.coe_Ici {α : Type u_1} [preorder α] (a : α) :
@[simp, norm_cast]
theorem finset.coe_Ioi {α : Type u_1} [preorder α] (a : α) :
def finset.Iic {α : Type u_1} [preorder α] (a : α) :

The finset of elements `x` such that `a ≤ x`. Basically `set.Iic a` as a finset.

Equations
def finset.Iio {α : Type u_1} [preorder α] (a : α) :

The finset of elements `x` such that `a < x`. Basically `set.Iio a` as a finset.

Equations
@[simp]
theorem finset.mem_Iic {α : Type u_1} [preorder α] {a x : α} :
x x a
@[simp]
theorem finset.mem_Iio {α : Type u_1} [preorder α] {a x : α} :
x x < a
@[simp, norm_cast]
theorem finset.coe_Iic {α : Type u_1} [preorder α] (a : α) :
@[simp, norm_cast]
theorem finset.coe_Iio {α : Type u_1} [preorder α] (a : α) :
@[protected, instance]
Equations
theorem finset.Ici_eq_Icc {α : Type u_1} [preorder α] [order_top α] (a : α) :
theorem finset.Ioi_eq_Ioc {α : Type u_1} [preorder α] [order_top α] (a : α) :
@[protected, instance]
Equations
theorem finset.Iic_eq_Icc {α : Type u_1} [preorder α] [order_bot α]  :
theorem finset.Iio_eq_Ico {α : Type u_1} [preorder α] [order_bot α]  :
def finset.uIcc {α : Type u_1} [lattice α] (a b : α) :

`finset.uIcc a b` is the set of elements lying between `a` and `b`, with `a` and `b` included. Note that we define it more generally in a lattice as `finset.Icc (a ⊓ b) (a ⊔ b)`. In a product type, `finset.uIcc` corresponds to the bounding box of the two elements.

Equations
@[simp]
theorem finset.mem_uIcc {α : Type u_1} [lattice α] {a b x : α} :
x b a b x x a b
@[simp, norm_cast]
theorem finset.coe_uIcc {α : Type u_1} [lattice α] (a b : α) :
b) = b

### Intervals as multisets #

def multiset.Icc {α : Type u_1} [preorder α] (a b : α) :

The multiset of elements `x` such that `a ≤ x` and `x ≤ b`. Basically `set.Icc a b` as a multiset.

Equations
def multiset.Ico {α : Type u_1} [preorder α] (a b : α) :

The multiset of elements `x` such that `a ≤ x` and `x < b`. Basically `set.Ico a b` as a multiset.

Equations
def multiset.Ioc {α : Type u_1} [preorder α] (a b : α) :

The multiset of elements `x` such that `a < x` and `x ≤ b`. Basically `set.Ioc a b` as a multiset.

Equations
def multiset.Ioo {α : Type u_1} [preorder α] (a b : α) :

The multiset of elements `x` such that `a < x` and `x < b`. Basically `set.Ioo a b` as a multiset.

Equations
@[simp]
theorem multiset.mem_Icc {α : Type u_1} [preorder α] {a b x : α} :
x b a x x b
@[simp]
theorem multiset.mem_Ico {α : Type u_1} [preorder α] {a b x : α} :
x b a x x < b
@[simp]
theorem multiset.mem_Ioc {α : Type u_1} [preorder α] {a b x : α} :
x b a < x x b
@[simp]
theorem multiset.mem_Ioo {α : Type u_1} [preorder α] {a b x : α} :
x b a < x x < b
def multiset.Ici {α : Type u_1} [preorder α] (a : α) :

The multiset of elements `x` such that `a ≤ x`. Basically `set.Ici a` as a multiset.

Equations
def multiset.Ioi {α : Type u_1} [preorder α] (a : α) :

The multiset of elements `x` such that `a < x`. Basically `set.Ioi a` as a multiset.

Equations
@[simp]
theorem multiset.mem_Ici {α : Type u_1} [preorder α] {a x : α} :
a x
@[simp]
theorem multiset.mem_Ioi {α : Type u_1} [preorder α] {a x : α} :
a < x
def multiset.Iic {α : Type u_1} [preorder α] (b : α) :

The multiset of elements `x` such that `x ≤ b`. Basically `set.Iic b` as a multiset.

Equations
def multiset.Iio {α : Type u_1} [preorder α] (b : α) :

The multiset of elements `x` such that `x < b`. Basically `set.Iio b` as a multiset.

Equations
@[simp]
theorem multiset.mem_Iic {α : Type u_1} [preorder α] {b x : α} :
x b
@[simp]
theorem multiset.mem_Iio {α : Type u_1} [preorder α] {b x : α} :
x < b

### Finiteness of `set` intervals #

@[protected, instance]
def set.fintype_Icc {α : Type u_1} [preorder α] (a b : α) :
Equations
• = _
@[protected, instance]
def set.fintype_Ico {α : Type u_1} [preorder α] (a b : α) :
Equations
• = _
@[protected, instance]
def set.fintype_Ioc {α : Type u_1} [preorder α] (a b : α) :
Equations
• = _
@[protected, instance]
def set.fintype_Ioo {α : Type u_1} [preorder α] (a b : α) :
Equations
• = _
theorem set.finite_Icc {α : Type u_1} [preorder α] (a b : α) :
theorem set.finite_Ico {α : Type u_1} [preorder α] (a b : α) :
theorem set.finite_Ioc {α : Type u_1} [preorder α] (a b : α) :
theorem set.finite_Ioo {α : Type u_1} [preorder α] (a b : α) :
@[protected, instance]
def set.fintype_Ici {α : Type u_1} [preorder α] (a : α) :
Equations
@[protected, instance]
def set.fintype_Ioi {α : Type u_1} [preorder α] (a : α) :
Equations
theorem set.finite_Ici {α : Type u_1} [preorder α] (a : α) :
theorem set.finite_Ioi {α : Type u_1} [preorder α] (a : α) :
@[protected, instance]
def set.fintype_Iic {α : Type u_1} [preorder α] (b : α) :
Equations
@[protected, instance]
def set.fintype_Iio {α : Type u_1} [preorder α] (b : α) :
Equations
theorem set.finite_Iic {α : Type u_1} [preorder α] (b : α) :
theorem set.finite_Iio {α : Type u_1} [preorder α] (b : α) :
@[protected, instance]
def set.fintype_uIcc {α : Type u_1} [lattice α] (a b : α) :
Equations
• = _
@[simp]
theorem set.finite_interval {α : Type u_1} [lattice α] (a b : α) :

### Instances #

noncomputable def locally_finite_order.of_finite_Icc {α : Type u_1} [preorder α] (h : (a b : α), (set.Icc a b).finite) :

A noncomputable constructor from the finiteness of all closed intervals.

Equations
@[reducible]
def fintype.to_locally_finite_order {α : Type u_1} [preorder α] [fintype α]  :

A fintype is a locally finite order.

This is not an instance as it would not be defeq to better instances such as `fin.locally_finite_order`.

Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected]
noncomputable def order_embedding.locally_finite_order {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ↪o β) :

Given an order embedding `α ↪o β`, pulls back the `locally_finite_order` on `β` to `α`.

Equations
@[protected, instance]

Note we define `Icc (to_dual a) (to_dual b)` as `Icc α _ _ b a` (which has type `finset α` not `finset αᵒᵈ`!) instead of `(Icc b a).map to_dual.to_embedding` as this means the following is defeq:

``````lemma this : (Icc (to_dual (to_dual a)) (to_dual (to_dual b)) : _) = (Icc a b : _) := rfl
``````
Equations
theorem Icc_to_dual {α : Type u_1} [preorder α] (a b : α) :
theorem Ico_to_dual {α : Type u_1} [preorder α] (a b : α) :
theorem Ioc_to_dual {α : Type u_1} [preorder α] (a b : α) :
theorem Ioo_to_dual {α : Type u_1} [preorder α] (a b : α) :
theorem Icc_of_dual {α : Type u_1} [preorder α] (a b : αᵒᵈ) :
theorem Ico_of_dual {α : Type u_1} [preorder α] (a b : αᵒᵈ) :
theorem Ioc_of_dual {α : Type u_1} [preorder α] (a b : αᵒᵈ) :
theorem Ioo_of_dual {α : Type u_1} [preorder α] (a b : αᵒᵈ) :
@[protected, instance]

Note we define `Iic (to_dual a)` as `Ici a` (which has type `finset α` not `finset αᵒᵈ`!) instead of `(Ici a).map to_dual.to_embedding` as this means the following is defeq:

``````lemma this : (Iic (to_dual (to_dual a)) : _) = (Iic a : _) := rfl
``````
Equations
theorem Iic_to_dual {α : Type u_1} [preorder α] (a : α) :
theorem Iio_to_dual {α : Type u_1} [preorder α] (a : α) :
theorem Ici_of_dual {α : Type u_1} [preorder α] (a : αᵒᵈ) :
theorem Ioi_of_dual {α : Type u_1} [preorder α] (a : αᵒᵈ) :
@[protected, instance]

Note we define `Ici (to_dual a)` as `Iic a` (which has type `finset α` not `finset αᵒᵈ`!) instead of `(Iic a).map to_dual.to_embedding` as this means the following is defeq:

``````lemma this : (Ici (to_dual (to_dual a)) : _) = (Ici a : _) := rfl
``````
Equations
theorem Ici_to_dual {α : Type u_1} [preorder α] (a : α) :
theorem Ioi_to_dual {α : Type u_1} [preorder α] (a : α) :
theorem Iic_of_dual {α : Type u_1} [preorder α] (a : αᵒᵈ) :
theorem Iio_of_dual {α : Type u_1} [preorder α] (a : αᵒᵈ) :
@[protected, instance]
def prod.locally_finite_order {α : Type u_1} {β : Type u_2} [preorder α] [preorder β]  :
Equations
@[protected, instance]
def prod.locally_finite_order_top {α : Type u_1} {β : Type u_2} [preorder α] [preorder β]  :
Equations
@[protected, instance]
def prod.locally_finite_order_bot {α : Type u_1} {β : Type u_2} [preorder α] [preorder β]  :
Equations
theorem prod.Icc_eq {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (p q : α × β) :
q = q.fst ×ˢ q.snd
@[simp]
theorem prod.Icc_mk_mk {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (a₁ a₂ : α) (b₁ b₂ : β) :
finset.Icc (a₁, b₁) (a₂, b₂) = a₂ ×ˢ b₂
theorem prod.card_Icc {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (p q : α × β) :
q).card = q.fst).card * q.snd).card
theorem prod.uIcc_eq {α : Type u_1} {β : Type u_2} [lattice α] [lattice β] (p q : α × β) :
q = q.fst ×ˢ q.snd
@[simp]
theorem prod.uIcc_mk_mk {α : Type u_1} {β : Type u_2} [lattice α] [lattice β] (a₁ a₂ : α) (b₁ b₂ : β) :
finset.uIcc (a₁, b₁) (a₂, b₂) = a₂ ×ˢ b₂
theorem prod.card_uIcc {α : Type u_1} {β : Type u_2} [lattice α] [lattice β] (p q : α × β) :
q).card = q.fst).card * q.snd).card

#### `with_top`, `with_bot`#

Adding a `⊤` to a locally finite `order_top` keeps it locally finite. Adding a `⊥` to a locally finite `order_bot` keeps it locally finite.

@[protected, instance]
def with_top.locally_finite_order (α : Type u_1) [order_top α]  :
Equations
• = {finset_Icc := λ (a b : with_top α), with_top.locally_finite_order._match_1 α a b, finset_Ico := λ (a b : with_top α), with_top.locally_finite_order._match_2 α a b, finset_Ioc := λ (a b : with_top α), with_top.locally_finite_order._match_3 α a b, finset_Ioo := λ (a b : with_top α), with_top.locally_finite_order._match_4 α a b, finset_mem_Icc := _, finset_mem_Ico := _, finset_mem_Ioc := _, finset_mem_Ioo := _}
• with_top.locally_finite_order._match_1 α a b =
• with_top.locally_finite_order._match_1 α a =
• with_top.locally_finite_order._match_1 α b =
• with_top.locally_finite_order._match_1 α = {}
• with_top.locally_finite_order._match_2 α a b =
• with_top.locally_finite_order._match_2 α a =
• with_top.locally_finite_order._match_2 α _x =
• with_top.locally_finite_order._match_3 α a b =
• with_top.locally_finite_order._match_3 α a =
• with_top.locally_finite_order._match_3 α _x =
• with_top.locally_finite_order._match_4 α a b =
• with_top.locally_finite_order._match_4 α a =
• with_top.locally_finite_order._match_4 α _x =
theorem with_top.Icc_coe_top (α : Type u_1) [order_top α] (a : α) :
theorem with_top.Icc_coe_coe (α : Type u_1) [order_top α] (a b : α) :
theorem with_top.Ico_coe_top (α : Type u_1) [order_top α] (a : α) :
theorem with_top.Ico_coe_coe (α : Type u_1) [order_top α] (a b : α) :
theorem with_top.Ioc_coe_top (α : Type u_1) [order_top α] (a : α) :
theorem with_top.Ioc_coe_coe (α : Type u_1) [order_top α] (a b : α) :
theorem with_top.Ioo_coe_top (α : Type u_1) [order_top α] (a : α) :
theorem with_top.Ioo_coe_coe (α : Type u_1) [order_top α] (a b : α) :
@[protected, instance]
def with_bot.locally_finite_order (α : Type u_1) [order_bot α]  :
Equations
theorem with_bot.Icc_bot_coe (α : Type u_1) [order_bot α] (b : α) :
theorem with_bot.Icc_coe_coe (α : Type u_1) [order_bot α] (a b : α) :
theorem with_bot.Ico_bot_coe (α : Type u_1) [order_bot α] (b : α) :
theorem with_bot.Ico_coe_coe (α : Type u_1) [order_bot α] (a b : α) :
theorem with_bot.Ioc_bot_coe (α : Type u_1) [order_bot α] (b : α) :
theorem with_bot.Ioc_coe_coe (α : Type u_1) [order_bot α] (a b : α) :
theorem with_bot.Ioo_bot_coe (α : Type u_1) [order_bot α] (b : α) :
theorem with_bot.Ioo_coe_coe (α : Type u_1) [order_bot α] (a b : α) :

#### Transfer locally finite orders across order isomorphisms #

@[reducible]
def order_iso.locally_finite_order {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) :

Transfer `locally_finite_order` across an `order_iso`.

Equations
@[reducible]
def order_iso.locally_finite_order_top {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) :

Transfer `locally_finite_order_top` across an `order_iso`.

Equations
@[reducible]
def order_iso.locally_finite_order_bot {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (f : α ≃o β) :

Transfer `locally_finite_order_bot` across an `order_iso`.

Equations

#### Subtype of a locally finite order #

@[protected, instance]
def subtype.locally_finite_order {α : Type u_1} [preorder α] (p : α Prop)  :
Equations
@[protected, instance]
def subtype.locally_finite_order_top {α : Type u_1} [preorder α] (p : α Prop)  :
Equations
@[protected, instance]
def subtype.locally_finite_order_bot {α : Type u_1} [preorder α] (p : α Prop)  :
Equations
theorem finset.subtype_Icc_eq {α : Type u_1} [preorder α] (p : α Prop) (a b : subtype p) :
b = b)
theorem finset.subtype_Ico_eq {α : Type u_1} [preorder α] (p : α Prop) (a b : subtype p) :
b = b)
theorem finset.subtype_Ioc_eq {α : Type u_1} [preorder α] (p : α Prop) (a b : subtype p) :
b = b)
theorem finset.subtype_Ioo_eq {α : Type u_1} [preorder α] (p : α Prop) (a b : subtype p) :
b = b)
theorem finset.map_subtype_embedding_Icc {α : Type u_1} [preorder α] (p : α Prop) (a b : subtype p) (hp : ⦃a b x : α⦄, a x x b p a p b p x) :
= b
theorem finset.map_subtype_embedding_Ico {α : Type u_1} [preorder α] (p : α Prop) (a b : subtype p) (hp : ⦃a b x : α⦄, a x x b p a p b p x) :
= b
theorem finset.map_subtype_embedding_Ioc {α : Type u_1} [preorder α] (p : α Prop) (a b : subtype p) (hp : ⦃a b x : α⦄, a x x b p a p b p x) :
= b
theorem finset.map_subtype_embedding_Ioo {α : Type u_1} [preorder α] (p : α Prop) (a b : subtype p) (hp : ⦃a b x : α⦄, a x x b p a p b p x) :
= b
theorem finset.subtype_Ici_eq {α : Type u_1} [preorder α] (p : α Prop) (a : subtype p) :
=
theorem finset.subtype_Ioi_eq {α : Type u_1} [preorder α] (p : α Prop) (a : subtype p) :
=
theorem finset.map_subtype_embedding_Ici {α : Type u_1} [preorder α] (p : α Prop) (a : subtype p) (hp : ⦃a x : α⦄, a x p a p x) :
theorem finset.map_subtype_embedding_Ioi {α : Type u_1} [preorder α] (p : α Prop) (a : subtype p) (hp : ⦃a x : α⦄, a x p a p x) :
theorem finset.subtype_Iic_eq {α : Type u_1} [preorder α] (p : α Prop) (a : subtype p) :
=
theorem finset.subtype_Iio_eq {α : Type u_1} [preorder α] (p : α Prop) (a : subtype p) :
=
theorem finset.map_subtype_embedding_Iic {α : Type u_1} [preorder α] (p : α Prop) (a : subtype p) (hp : ⦃a x : α⦄, x a p a p x) :
theorem finset.map_subtype_embedding_Iio {α : Type u_1} [preorder α] (p : α Prop) (a : subtype p) (hp : ⦃a x : α⦄, x a p a p x) :