Locally finite orders #
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.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.
When it's also an 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.
When it's also an 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 it is noncomputable). See
fintype.to_locally_finite_order
. - from a definition of
finset.Icc
alone. Seelocally_finite_order.of_Icc
. - by pulling back
locally_finite_order β
through an order embeddingf : α →o β
. Seeorder_embedding.locally_finite_order
.
Instances for concrete types are proved in their respective files:
ℕ
is indata.nat.interval
ℤ
is indata.int.interval
ℕ+
is indata.pnat.interval
fin n
is indata.fin.interval
finset α
is indata.finset.interval
Σ i, α i
is indata.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.
- finset_Icc : α → α → finset α
- finset_Ico : α → α → finset α
- finset_Ioc : α → α → finset α
- finset_Ioo : α → α → finset α
- finset_mem_Icc : ∀ (a b x : α), x ∈ locally_finite_order.finset_Icc a b ↔ a ≤ x ∧ x ≤ b
- finset_mem_Ico : ∀ (a b x : α), x ∈ locally_finite_order.finset_Ico a b ↔ a ≤ x ∧ x < b
- finset_mem_Ioc : ∀ (a b x : α), x ∈ locally_finite_order.finset_Ioc a b ↔ a < x ∧ x ≤ b
- finset_mem_Ioo : ∀ (a b x : α), x ∈ locally_finite_order.finset_Ioo a b ↔ a < x ∧ x < b
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
.
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
- locally_finite_order.of_Icc' α finset_Icc mem_Icc = {finset_Icc := finset_Icc, finset_Ico := λ (a b : α), finset.filter (λ (x : α), ¬b ≤ x) (finset_Icc a b), finset_Ioc := λ (a b : α), finset.filter (λ (x : α), ¬x ≤ a) (finset_Icc a b), finset_Ioo := λ (a b : α), finset.filter (λ (x : α), ¬x ≤ a ∧ ¬b ≤ x) (finset_Icc a b), finset_mem_Icc := mem_Icc, finset_mem_Ico := _, finset_mem_Ioc := _, finset_mem_Ioo := _}
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
- locally_finite_order.of_Icc α finset_Icc mem_Icc = {finset_Icc := finset_Icc, finset_Ico := λ (a b : α), finset.filter (λ (x : α), x ≠ b) (finset_Icc a b), finset_Ioc := λ (a b : α), finset.filter (λ (x : α), a ≠ x) (finset_Icc a b), finset_Ioo := λ (a b : α), finset.filter (λ (x : α), a ≠ x ∧ x ≠ b) (finset_Icc a b), finset_mem_Icc := mem_Icc, finset_mem_Ico := _, finset_mem_Ioc := _, finset_mem_Ioo := _}
Intervals as finsets #
The finset of elements x
such that a ≤ x
and x ≤ b
. Basically set.Icc a b
as a finset.
Equations
The finset of elements x
such that a ≤ x
and x < b
. Basically set.Ico a b
as a finset.
Equations
The finset of elements x
such that a < x
and x ≤ b
. Basically set.Ioc a b
as a finset.
Equations
The finset of elements x
such that a < x
and x < b
. Basically set.Ioo a b
as a finset.
Equations
The finset of elements x
such that a ≤ x
. Basically set.Ici a
as a finset.
Equations
- finset.Ici a = finset.Icc a ⊤
The finset of elements x
such that a < x
. Basically set.Ioi a
as a finset.
Equations
- finset.Ioi a = finset.Ioc a ⊤
The finset of elements x
such that x ≤ b
. Basically set.Iic b
as a finset.
Equations
- finset.Iic b = finset.Icc ⊥ b
The finset of elements x
such that x < b
. Basically set.Iio b
as a finset.
Equations
- finset.Iio b = finset.Ico ⊥ b
Intervals as multisets #
The multiset of elements x
such that a ≤ x
and x ≤ b
. Basically set.Icc a b
as a
multiset.
Equations
- multiset.Icc a b = (finset.Icc a b).val
The multiset of elements x
such that a ≤ x
and x < b
. Basically set.Ico a b
as a
multiset.
Equations
- multiset.Ico a b = (finset.Ico a b).val
The multiset of elements x
such that a < x
and x ≤ b
. Basically set.Ioc a b
as a
multiset.
Equations
- multiset.Ioc a b = (finset.Ioc a b).val
The multiset of elements x
such that a < x
and x < b
. Basically set.Ioo a b
as a
multiset.
Equations
- multiset.Ioo a b = (finset.Ioo a b).val
The multiset of elements x
such that a ≤ x
. Basically set.Ici a
as a multiset.
Equations
- multiset.Ici a = (finset.Ici a).val
The multiset of elements x
such that a < x
. Basically set.Ioi a
as a multiset.
Equations
- multiset.Ioi a = (finset.Ioi a).val
The multiset of elements x
such that x ≤ b
. Basically set.Iic b
as a multiset.
Equations
- multiset.Iic b = (finset.Iic b).val
The multiset of elements x
such that x < b
. Basically set.Iio b
as a multiset.
Equations
- multiset.Iio b = (finset.Iio b).val
Equations
- set.fintype_Icc a b = fintype.of_finset (finset.Icc a b) _
Equations
- set.fintype_Ico a b = fintype.of_finset (finset.Ico a b) _
Equations
- set.fintype_Ioc a b = fintype.of_finset (finset.Ioc a b) _
Equations
- set.fintype_Ioo a b = fintype.of_finset (finset.Ioo a b) _
Equations
- set.fintype_Ici a = fintype.of_finset (finset.Ici a) _
Equations
- set.fintype_Ioi a = fintype.of_finset (finset.Ioi a) _
Equations
- set.fintype_Iic b = fintype.of_finset (finset.Iic b) _
Equations
- set.fintype_Iio b = fintype.of_finset (finset.Iio b) _
Instances #
A noncomputable constructor from the finiteness of all closed intervals.
Equations
- locally_finite_order.of_finite_Icc h = locally_finite_order.of_Icc' α (λ (a b : α), _.to_finset) _
A fintype is noncomputably a locally finite order.
Equations
- fintype.to_locally_finite_order = {finset_Icc := λ (a b : α), _.to_finset, finset_Ico := λ (a b : α), _.to_finset, finset_Ioc := λ (a b : α), _.to_finset, finset_Ioo := λ (a b : α), _.to_finset, finset_mem_Icc := _, finset_mem_Ico := _, finset_mem_Ioc := _, finset_mem_Ioo := _}
Given an order embedding α ↪o β
, pulls back the locally_finite_order
on β
to α
.
Equations
- f.locally_finite_order = {finset_Icc := λ (a b : α), (finset.Icc (⇑f a) (⇑f b)).preimage ⇑f _, finset_Ico := λ (a b : α), (finset.Ico (⇑f a) (⇑f b)).preimage ⇑f _, finset_Ioc := λ (a b : α), (finset.Ioc (⇑f a) (⇑f b)).preimage ⇑f _, finset_Ioo := λ (a b : α), (finset.Ioo (⇑f a) (⇑f b)).preimage ⇑f _, finset_mem_Icc := _, finset_mem_Ico := _, finset_mem_Ioc := _, finset_mem_Ioo := _}
Note we define Icc (to_dual a) (to_dual b)
as Icc α _ _ b a
(which has type finset α
not
finset (order_dual α)
!) 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
- order_dual.locally_finite_order = {finset_Icc := λ (a b : order_dual α), finset.Icc (⇑order_dual.of_dual b) (⇑order_dual.of_dual a), finset_Ico := λ (a b : order_dual α), finset.Ioc (⇑order_dual.of_dual b) (⇑order_dual.of_dual a), finset_Ioc := λ (a b : order_dual α), finset.Ico (⇑order_dual.of_dual b) (⇑order_dual.of_dual a), finset_Ioo := λ (a b : order_dual α), finset.Ioo (⇑order_dual.of_dual b) (⇑order_dual.of_dual a), finset_mem_Icc := _, finset_mem_Ico := _, finset_mem_Ioc := _, finset_mem_Ioo := _}
Equations
- prod.locally_finite_order = locally_finite_order.of_Icc' (α × β) (λ (a b : α × β), (finset.Icc a.fst b.fst).product (finset.Icc a.snd b.snd)) prod.locally_finite_order._proof_1
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.
Equations
- with_top.locally_finite_order α = {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 = finset.map function.embedding.coe_option (finset.Icc a b)
- with_top.locally_finite_order._match_1 α ↑a ⊤ = ⇑finset.insert_none (finset.Ici 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 = finset.map function.embedding.coe_option (finset.Ico a b)
- with_top.locally_finite_order._match_2 α ↑a ⊤ = finset.map function.embedding.coe_option (finset.Ici a)
- with_top.locally_finite_order._match_2 α ⊤ _x = ∅
- with_top.locally_finite_order._match_3 α ↑a ↑b = finset.map function.embedding.coe_option (finset.Ioc a b)
- with_top.locally_finite_order._match_3 α ↑a ⊤ = ⇑finset.insert_none (finset.Ioi a)
- with_top.locally_finite_order._match_3 α ⊤ _x = ∅
- with_top.locally_finite_order._match_4 α ↑a ↑b = finset.map function.embedding.coe_option (finset.Ioo a b)
- with_top.locally_finite_order._match_4 α ↑a ⊤ = finset.map function.embedding.coe_option (finset.Ioi a)
- with_top.locally_finite_order._match_4 α ⊤ _x = ∅
Subtype of a locally finite order #
Equations
- subtype.locally_finite_order p = {finset_Icc := λ (a b : subtype p), finset.subtype p (finset.Icc ↑a ↑b), finset_Ico := λ (a b : subtype p), finset.subtype p (finset.Ico ↑a ↑b), finset_Ioc := λ (a b : subtype p), finset.subtype p (finset.Ioc ↑a ↑b), finset_Ioo := λ (a b : subtype p), finset.subtype p (finset.Ioo ↑a ↑b), finset_mem_Icc := _, finset_mem_Ico := _, finset_mem_Ioc := _, finset_mem_Ioo := _}