doc-next-gen

Mathlib.Order.Interval.Finset.Defs

Module docstring

{"# 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 Mathlib.Order.Interval.Finset.Basic.

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 LocallyFiniteOrder, * 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.

In a LocallyFiniteOrderTop, * Finset.Ici: Closed-infinite interval as a finset. * Finset.Ioi: Open-infinite interval as a finset.

In a LocallyFiniteOrderBot, * Finset.Iic: Infinite-open interval as a finset. * Finset.Iio: Infinite-closed interval as a finset.

Instances

A LocallyFiniteOrder instance can be built * for a subtype of a locally finite order. See Subtype.locallyFiniteOrder. * for the product of two locally finite orders. See Prod.locallyFiniteOrder. * for any fintype (but not as an instance). See Fintype.toLocallyFiniteOrder. * from a definition of Finset.Icc alone. See LocallyFiniteOrder.ofIcc. * by pulling back LocallyFiniteOrder β through an order embedding f : α →o β. See OrderEmbedding.locallyFiniteOrder.

Instances for concrete types are proved in their respective files: * ℕ is in Order.Interval.Finset.Nat * ℤ is in Data.Int.Interval * ℕ+ is in Data.PNat.Interval * Fin n is in Order.Interval.Finset.Fin * 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 LocallyFiniteOrder instance for α ×ₗ β where LocallyFiniteOrder α and Fintype β.

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

From LinearOrder α, NoMaxOrder α, LocallyFiniteOrder α, we can also define an order isomorphism α ≃ ℕ or α ≃ ℤ, depending on whether we have OrderBot α or NoMinOrder α and Nonempty α. When OrderBot α, we can match a : α to #(Iio a).

We can provide SuccOrder α from LinearOrder α and LocallyFiniteOrder α using

lean lemma exists_min_greater [LinearOrder α] [LocallyFiniteOrder α] {x ub : α} (hx : x < ub) : ∃ lub, x < lub ∧ ∀ y, x < y → lub ≤ y := by -- very non golfed have h : (Finset.Ioc x ub).Nonempty := ⟨ub, Finset.mem_Ioc.2 ⟨hx, le_rfl⟩⟩ use Finset.min' (Finset.Ioc x ub) h constructor · exact (Finset.mem_Ioc.mp <| Finset.min'_mem _ h).1 rintro y hxy obtain hy | hy := le_total y ub · refine Finset.min'_le (Ioc x ub) y ?_ simp [*] at * · exact (Finset.min'_le _ _ (Finset.mem_Ioc.2 ⟨hx, le_rfl⟩)).trans hy 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 SuccOrder, but it's not locally finite as Icc (-1) 1 is infinite. ","### Intervals as finsets ","### Finiteness of Set intervals ","### Instances ","### OrderDual ","### Prod ","#### WithTop, WithBot

Adding a ⊤ to a locally finite OrderTop keeps it locally finite. Adding a ⊥ to a locally finite OrderBot keeps it locally finite. ","#### Transfer locally finite orders across order isomorphisms ","#### Subtype of a locally finite order ","We make the instances below low priority so when alternative constructions are available they are preferred. "}

LocallyFiniteOrder structure
(α : Type*) [Preorder α]
Full source 
/-- This is a mixin class describing a locally finite order,
that is, is an order where bounded intervals are finite.
When you don't care too much about definitional equality, you can use `LocallyFiniteOrder.ofIcc` or
`LocallyFiniteOrder.ofFiniteIcc` to build a locally finite order from just `Finset.Icc`. -/
class LocallyFiniteOrder (α : Type*) [Preorder α] where
  /-- Left-closed right-closed interval -/
  finsetIcc : α → α → Finset α
  /-- Left-closed right-open interval -/
  finsetIco : α → α → Finset α
  /-- Left-open right-closed interval -/
  finsetIoc : α → α → Finset α
  /-- Left-open right-open interval -/
  finsetIoo : α → α → Finset α
  /-- `x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b` -/
  finset_mem_Icc : ∀ a b x : α, x ∈ finsetIcc a bx ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
  /-- `x ∈ finsetIco a b ↔ a ≤ x ∧ x < b` -/
  finset_mem_Ico : ∀ a b x : α, x ∈ finsetIco a bx ∈ finsetIco a b ↔ a ≤ x ∧ x < b
  /-- `x ∈ finsetIoc a b ↔ a < x ∧ x ≤ b` -/
  finset_mem_Ioc : ∀ a b x : α, x ∈ finsetIoc a bx ∈ finsetIoc a b ↔ a < x ∧ x ≤ b
  /-- `x ∈ finsetIoo a b ↔ a < x ∧ x < b` -/
  finset_mem_Ioo : ∀ a b x : α, x ∈ finsetIoo a bx ∈ finsetIoo a b ↔ a < x ∧ x < b
Locally Finite Order
Informal description
A locally finite order is a preorder $\alpha$ where every bounded interval is finite. This means that for any two elements $a, b \in \alpha$, the intervals $[a, b]$, $[a, b)$, $(a, b]$, and $(a, b)$ are all finite sets. This property allows us to represent these intervals as finite sets (e.g., finsets) and perform operations on them.
LocallyFiniteOrderTop structure
(α : Type*) [Preorder α]
Full source 
/-- This mixin class describes an order where all intervals bounded below are finite. This is
slightly weaker than `LocallyFiniteOrder` + `OrderTop` as it allows empty types. -/
class LocallyFiniteOrderTop (α : Type*) [Preorder α] where
  /-- Left-open right-infinite interval -/
  finsetIoi : α → Finset α
  /-- Left-closed right-infinite interval -/
  finsetIci : α → Finset α
  /-- `x ∈ finsetIci a ↔ a ≤ x` -/
  finset_mem_Ici : ∀ a x : α, x ∈ finsetIci ax ∈ finsetIci a ↔ a ≤ x
  /-- `x ∈ finsetIoi a ↔ a < x` -/
  finset_mem_Ioi : ∀ a x : α, x ∈ finsetIoi ax ∈ finsetIoi a ↔ a < x
Locally finite order with finite intervals bounded below
Informal description
A structure representing an order where all intervals bounded below are finite. This is a weaker condition than requiring the order to be locally finite with a top element, as it allows for empty types.
LocallyFiniteOrderBot structure
(α : Type*) [Preorder α]
Full source 
/-- This mixin class describes an order where all intervals bounded above are finite. This is
slightly weaker than `LocallyFiniteOrder` + `OrderBot` as it allows empty types. -/
class LocallyFiniteOrderBot (α : Type*) [Preorder α] where
  /-- Left-infinite right-open interval -/
  finsetIio : α → Finset α
  /-- Left-infinite right-closed interval -/
  finsetIic : α → Finset α
  /-- `x ∈ finsetIic a ↔ x ≤ a` -/
  finset_mem_Iic : ∀ a x : α, x ∈ finsetIic ax ∈ finsetIic a ↔ x ≤ a
  /-- `x ∈ finsetIio a ↔ x < a` -/
  finset_mem_Iio : ∀ a x : α, x ∈ finsetIio ax ∈ finsetIio a ↔ x < a
Locally finite order with finite lower-bounded intervals
Informal description
A structure representing an order where all intervals bounded below are finite. This is slightly weaker than requiring both `LocallyFiniteOrder` and `OrderBot` structures, as it allows for empty types.
LocallyFiniteOrder.ofIcc' definition
(α : Type*) [Preorder α] [DecidableLE α] (finsetIcc : α → α → Finset α) (mem_Icc : ∀ a b x, x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b) : LocallyFiniteOrder α
Full source 
/-- A constructor from a definition of `Finset.Icc` alone, the other ones being derived by removing
the ends. As opposed to `LocallyFiniteOrder.ofIcc`, this one requires `DecidableLE` but
only `Preorder`. -/
def LocallyFiniteOrder.ofIcc' (α : Type*) [Preorder α] [DecidableLE α]
    (finsetIcc : α → α → Finset α) (mem_Icc : ∀ a b x, x ∈ finsetIcc a bx ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b) :
    LocallyFiniteOrder α where
  finsetIcc := finsetIcc
  finsetIco a b := {x ∈ finsetIcc a b | ¬b ≤ x}
  finsetIoc a b := {x ∈ finsetIcc a b | ¬x ≤ a}
  finsetIoo a b := {x ∈ finsetIcc a b | ¬x ≤ a ∧ ¬b ≤ x}
  finset_mem_Icc := mem_Icc
  finset_mem_Ico a b x := by rw [Finset.mem_filter, mem_Icc, and_assoc, lt_iff_le_not_le]
  finset_mem_Ioc a b x := by rw [Finset.mem_filter, mem_Icc, and_right_comm, lt_iff_le_not_le]
  finset_mem_Ioo a b x := by
    rw [Finset.mem_filter, mem_Icc, and_and_and_comm, lt_iff_le_not_le, lt_iff_le_not_le]
Construction of locally finite order from closed intervals with decidable order
Informal description
Given a preorder $\alpha$ with a decidable $\leq$ relation, a function `finsetIcc` that constructs the closed interval $[a, b]$ as a finite set for any $a, b \in \alpha$, and a proof that for any $x \in \alpha$, $x \in \text{finsetIcc } a b$ if and only if $a \leq x \leq b$, this constructs a locally finite order structure on $\alpha$. The other interval constructions (open-closed, closed-open, and open-open) are derived from `finsetIcc` by filtering out the endpoints as follows: - The closed-open interval $[a, b)$ consists of elements in $[a, b]$ that are not greater than or equal to $b$. - The open-closed interval $(a, b]$ consists of elements in $[a, b]$ that are not less than or equal to $a$. - The open-open interval $(a, b)$ consists of elements in $[a, b]$ that are neither less than or equal to $a$ nor greater than or equal to $b$.
LocallyFiniteOrder.ofIcc definition
(α : Type*) [PartialOrder α] [DecidableEq α] (finsetIcc : α → α → Finset α) (mem_Icc : ∀ a b x, x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b) : LocallyFiniteOrder α
Full source 
/-- A constructor from a definition of `Finset.Icc` alone, the other ones being derived by removing
the ends. As opposed to `LocallyFiniteOrder.ofIcc'`, this one requires `PartialOrder` but only
`DecidableEq`. -/
def LocallyFiniteOrder.ofIcc (α : Type*) [PartialOrder α] [DecidableEq α]
    (finsetIcc : α → α → Finset α) (mem_Icc : ∀ a b x, x ∈ finsetIcc a bx ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b) :
    LocallyFiniteOrder α where
  finsetIcc := finsetIcc
  finsetIco a b := {x ∈ finsetIcc a b | x ≠ b}
  finsetIoc a b := {x ∈ finsetIcc a b | a ≠ x}
  finsetIoo a b := {x ∈ finsetIcc a b | a ≠ x ∧ x ≠ b}
  finset_mem_Icc := mem_Icc
  finset_mem_Ico a b x := by rw [Finset.mem_filter, mem_Icc, and_assoc, lt_iff_le_and_ne]
  finset_mem_Ioc a b x := by rw [Finset.mem_filter, mem_Icc, and_right_comm, lt_iff_le_and_ne]
  finset_mem_Ioo a b x := by
    rw [Finset.mem_filter, mem_Icc, and_and_and_comm, lt_iff_le_and_ne, lt_iff_le_and_ne]
Construction of locally finite order from closed intervals
Informal description
Given a partially ordered set $\alpha$ with decidable equality, and a function `finsetIcc` that constructs the closed interval $[a, b]$ as a finite set for any $a, b \in \alpha$, satisfying the property that for any $x \in \alpha$, $x \in \text{finsetIcc } a b$ if and only if $a \leq x \leq b$, this constructs a locally finite order structure on $\alpha$. The other interval constructions (open-closed, closed-open, and open-open) are derived from `finsetIcc` by filtering out the endpoints.
LocallyFiniteOrderTop.ofIci' definition
(α : Type*) [Preorder α] [DecidableLE α] (finsetIci : α → Finset α) (mem_Ici : ∀ a x, x ∈ finsetIci a ↔ a ≤ x) : LocallyFiniteOrderTop α
Full source 
/-- A constructor from a definition of `Finset.Ici` alone, the other ones being derived by removing
the ends. As opposed to `LocallyFiniteOrderTop.ofIci`, this one requires `DecidableLE` but
only `Preorder`. -/
def LocallyFiniteOrderTop.ofIci' (α : Type*) [Preorder α] [DecidableLE α]
    (finsetIci : α → Finset α) (mem_Ici : ∀ a x, x ∈ finsetIci ax ∈ finsetIci a ↔ a ≤ x) :
    LocallyFiniteOrderTop α where
  finsetIci := finsetIci
  finsetIoi a := {x ∈ finsetIci a | ¬x ≤ a}
  finset_mem_Ici := mem_Ici
  finset_mem_Ioi a x := by rw [mem_filter, mem_Ici, lt_iff_le_not_le]
Construction of locally finite order from closed-infinite intervals
Informal description
Given a preorder $\alpha$ with decidable $\leq$ relation, a function `finsetIci` that constructs the closed-infinite interval $[a, \infty)$ as a finite set for any $a \in \alpha$, and a proof that for any $x \in \alpha$, $x \in \text{finsetIci } a$ if and only if $a \leq x$, this constructs a locally finite order structure on $\alpha$ where all intervals bounded below are finite. The open-infinite interval $(a, \infty)$ is derived from `finsetIci` by filtering out elements $x$ where $x \leq a$.
LocallyFiniteOrderTop.ofIci definition
(α : Type*) [PartialOrder α] [DecidableEq α] (finsetIci : α → Finset α) (mem_Ici : ∀ a x, x ∈ finsetIci a ↔ a ≤ x) : LocallyFiniteOrderTop α
Full source 
/-- A constructor from a definition of `Finset.Ici` alone, the other ones being derived by removing
the ends. As opposed to `LocallyFiniteOrderTop.ofIci'`, this one requires `PartialOrder` but
only `DecidableEq`. -/
def LocallyFiniteOrderTop.ofIci (α : Type*) [PartialOrder α] [DecidableEq α]
    (finsetIci : α → Finset α) (mem_Ici : ∀ a x, x ∈ finsetIci ax ∈ finsetIci a ↔ a ≤ x) :
    LocallyFiniteOrderTop α where
  finsetIci := finsetIci
  finsetIoi a := {x ∈ finsetIci a | a ≠ x}
  finset_mem_Ici := mem_Ici
  finset_mem_Ioi a x := by rw [mem_filter, mem_Ici, lt_iff_le_and_ne]
Constructor for locally finite order with finite upper intervals from `Ici` definition
Informal description
Given a partially ordered set $\alpha$ with decidable equality, a function `finsetIci` that constructs the closed-infinite interval $[a, \infty)$ as a finite set for any $a \in \alpha$, and a proof that for any $x \in \alpha$, $x \in \text{finsetIci } a$ if and only if $a \leq x$, this constructs a locally finite order structure on $\alpha$ where all intervals bounded below are finite. The open-infinite interval $(a, \infty)$ is derived from `finsetIci` by filtering out elements equal to $a$.
LocallyFiniteOrderBot.ofIic' definition
(α : Type*) [Preorder α] [DecidableLE α] (finsetIic : α → Finset α) (mem_Iic : ∀ a x, x ∈ finsetIic a ↔ x ≤ a) : LocallyFiniteOrderBot α
Full source 
/-- A constructor from a definition of `Finset.Iic` alone, the other ones being derived by removing
the ends. As opposed to `LocallyFiniteOrderBot.ofIic`, this one requires `DecidableLE` but
only `Preorder`. -/
def LocallyFiniteOrderBot.ofIic' (α : Type*) [Preorder α] [DecidableLE α]
    (finsetIic : α → Finset α) (mem_Iic : ∀ a x, x ∈ finsetIic ax ∈ finsetIic a ↔ x ≤ a) :
    LocallyFiniteOrderBot α where
  finsetIic := finsetIic
  finsetIio a := {x ∈ finsetIic a | ¬a ≤ x}
  finset_mem_Iic := mem_Iic
  finset_mem_Iio a x := by rw [mem_filter, mem_Iic, lt_iff_le_not_le]
Construction of locally finite order from infinite-closed intervals
Informal description
Given a preorder $\alpha$ with decidable $\leq$ relation, a function `finsetIic` that constructs the infinite-closed interval $(-\infty, a]$ as a finite set for any $a \in \alpha$, and a proof that for any $x \in \alpha$, $x \in \text{finsetIic } a$ if and only if $x \leq a$, this constructs a locally finite order structure on $\alpha$ where all intervals bounded above are finite. The infinite-open interval $(-\infty, a)$ is derived from `finsetIic` by filtering out elements $x$ where $a \leq x$.
LocallyFiniteOrderBot.ofIic definition
(α : Type*) [PartialOrder α] [DecidableEq α] (finsetIic : α → Finset α) (mem_Iic : ∀ a x, x ∈ finsetIic a ↔ x ≤ a) : LocallyFiniteOrderBot α
Full source 
/-- A constructor from a definition of `Finset.Iic` alone, the other ones being derived by removing
the ends. As opposed to `LocallyFiniteOrderBot.ofIic'`, this one requires `PartialOrder` but
only `DecidableEq`. -/
def LocallyFiniteOrderBot.ofIic (α : Type*) [PartialOrder α] [DecidableEq α]
    (finsetIic : α → Finset α) (mem_Iic : ∀ a x, x ∈ finsetIic ax ∈ finsetIic a ↔ x ≤ a) :
    LocallyFiniteOrderBot α where
  finsetIic := finsetIic
  finsetIio a := {x ∈ finsetIic a | x ≠ a}
  finset_mem_Iic := mem_Iic
  finset_mem_Iio a x := by rw [mem_filter, mem_Iic, lt_iff_le_and_ne]
Constructor for locally finite order with finite lower intervals from `Iic` definition
Informal description
Given a partially ordered type $\alpha$ with decidable equality, a constructor for `LocallyFiniteOrderBot` can be defined by specifying a function `finsetIic` that maps each element $a \in \alpha$ to a finite set containing all elements $x \leq a$, along with a proof that this function correctly characterizes the membership in the lower-closed interval. The other interval constructions (like lower-open intervals) are derived from this definition.
IsEmpty.toLocallyFiniteOrder abbrev
[Preorder α] [IsEmpty α] : LocallyFiniteOrder α
Full source 
/-- An empty type is locally finite.

This is not an instance as it would not be defeq to more specific instances. -/
protected abbrev IsEmpty.toLocallyFiniteOrder [Preorder α] [IsEmpty α] : LocallyFiniteOrder α where
  finsetIcc := isEmptyElim
  finsetIco := isEmptyElim
  finsetIoc := isEmptyElim
  finsetIoo := isEmptyElim
  finset_mem_Icc := isEmptyElim
  finset_mem_Ico := isEmptyElim
  finset_mem_Ioc := isEmptyElim
  finset_mem_Ioo := isEmptyElim
Empty Type is Locally Finite Order
Informal description
For any preorder $\alpha$ that is empty (i.e., has no elements), $\alpha$ is trivially a locally finite order. This means all bounded intervals in $\alpha$ are finite (in fact, empty).
IsEmpty.toLocallyFiniteOrderTop abbrev
[Preorder α] [IsEmpty α] : LocallyFiniteOrderTop α
Full source 
/-- An empty type is locally finite.

This is not an instance as it would not be defeq to more specific instances. -/
protected abbrev IsEmpty.toLocallyFiniteOrderTop [Preorder α] [IsEmpty α] :
    LocallyFiniteOrderTop α where
  finsetIci := isEmptyElim
  finsetIoi := isEmptyElim
  finset_mem_Ici := isEmptyElim
  finset_mem_Ioi := isEmptyElim
Empty Type Trivially Satisfies Locally Finite Order with Finite Upper-Bounded Intervals
Informal description
For any preorder $\alpha$ that is empty (i.e., has no elements), the structure `LocallyFiniteOrderTop` holds trivially, meaning all intervals bounded above are finite (in fact, empty).
IsEmpty.toLocallyFiniteOrderBot abbrev
[Preorder α] [IsEmpty α] : LocallyFiniteOrderBot α
Full source 
/-- An empty type is locally finite.

This is not an instance as it would not be defeq to more specific instances. -/
protected abbrev IsEmpty.toLocallyFiniteOrderBot [Preorder α] [IsEmpty α] :
    LocallyFiniteOrderBot α where
  finsetIic := isEmptyElim
  finsetIio := isEmptyElim
  finset_mem_Iic := isEmptyElim
  finset_mem_Iio := isEmptyElim
Empty Type Trivially Satisfies Locally Finite Order with Finite Lower-Bounded Intervals
Informal description
For any preorder $\alpha$ that is empty (i.e., has no elements), the structure `LocallyFiniteOrderBot` holds trivially, meaning all intervals bounded below are finite (in fact, empty).
Finset.Icc definition
(a b : α) : Finset α
Full source 
/-- The finset $[a, b]$ of elements `x` such that `a ≤ x` and `x ≤ b`. Basically `Set.Icc a b` as a
finset. -/
def Icc (a b : α) : Finset α :=
  LocallyFiniteOrder.finsetIcc a b
Closed interval as a finset
Informal description
For a locally finite order $\alpha$ and elements $a, b \in \alpha$, the finset $\text{Icc}(a, b)$ consists of all elements $x$ such that $a \leq x \leq b$. This is the finite set representation of the closed interval $[a, b]$.
Finset.Ico definition
(a b : α) : Finset α
Full source 
/-- The finset $[a, b)$ of elements `x` such that `a ≤ x` and `x < b`. Basically `Set.Ico a b` as a
finset. -/
def Ico (a b : α) : Finset α :=
  LocallyFiniteOrder.finsetIco a b
Closed-open interval as a finset
Informal description
For a locally finite order $\alpha$ and elements $a, b \in \alpha$, the finset $\text{Ico}(a, b)$ consists of all elements $x$ such that $a \leq x < b$. This is the finite set representation of the half-open interval $[a, b)$.
Finset.Ioc definition
(a b : α) : Finset α
Full source 
/-- The finset $(a, b]$ of elements `x` such that `a < x` and `x ≤ b`. Basically `Set.Ioc a b` as a
finset. -/
def Ioc (a b : α) : Finset α :=
  LocallyFiniteOrder.finsetIoc a b
Open-closed interval as a finset
Informal description
For a locally finite order $\alpha$ and elements $a, b \in \alpha$, the finset $\text{Ioc}(a, b)$ consists of all elements $x$ such that $a < x \leq b$. This is the finite set representation of the half-open interval $(a, b]$.
Finset.Ioo definition
(a b : α) : Finset α
Full source 
/-- The finset $(a, b)$ of elements `x` such that `a < x` and `x < b`. Basically `Set.Ioo a b` as a
finset. -/
def Ioo (a b : α) : Finset α :=
  LocallyFiniteOrder.finsetIoo a b
Open interval as a finset
Informal description
For a locally finite order $\alpha$ and elements $a, b \in \alpha$, the finset $\text{Ioo}(a, b)$ consists of all elements $x$ such that $a < x < b$. This is the finite set representation of the open interval $(a, b)$.
Finset.mem_Ico theorem
: x ∈ Ico a b ↔ a ≤ x ∧ x < b
Full source 
@[simp]
theorem mem_Ico : x ∈ Ico a bx ∈ Ico a b ↔ a ≤ x ∧ x < b :=
  LocallyFiniteOrder.finset_mem_Ico a b x
Membership in Closed-Open Interval Finset: $x \in \text{Ico}(a, b) \leftrightarrow a \leq x < b$
Informal description
For elements $x, a, b$ in a locally finite order $\alpha$, the element $x$ belongs to the closed-open interval finset $\text{Ico}(a, b)$ if and only if $a \leq x$ and $x < b$.
Finset.mem_Ioc theorem
: x ∈ Ioc a b ↔ a < x ∧ x ≤ b
Full source 
@[simp]
theorem mem_Ioc : x ∈ Ioc a bx ∈ Ioc a b ↔ a < x ∧ x ≤ b :=
  LocallyFiniteOrder.finset_mem_Ioc a b x
Membership in Open-Closed Interval Finset: $x \in \text{Ioc}(a, b) \leftrightarrow a < x \leq b$
Informal description
For elements $x, a, b$ in a locally finite order $\alpha$, the element $x$ belongs to the open-closed interval finset $\text{Ioc}(a, b)$ if and only if $a < x$ and $x \leq b$.
Finset.mem_Ioo theorem
: x ∈ Ioo a b ↔ a < x ∧ x < b
Full source 
@[simp]
theorem mem_Ioo : x ∈ Ioo a bx ∈ Ioo a b ↔ a < x ∧ x < b :=
  LocallyFiniteOrder.finset_mem_Ioo a b x
Membership in Open Interval Finset: $x \in \text{Ioo}(a, b) \leftrightarrow a < x < b$
Informal description
For elements $a, b, x$ in a locally finite order $\alpha$, the element $x$ belongs to the open interval finset $\text{Ioo}(a, b)$ if and only if $a < x$ and $x < b$.
Finset.coe_Icc theorem
(a b : α) : (Icc a b : Set α) = Set.Icc a b
Full source 
@[simp, norm_cast]
theorem coe_Icc (a b : α) : (Icc a b : Set α) = Set.Icc a b :=
  Set.ext fun _ => mem_Icc
Equality of Finset and Set Closed Intervals: $\text{Icc}(a, b) = [a, b]$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the underlying set of the closed interval finset $\text{Icc}(a, b)$ is equal to the set-theoretic closed interval $\text{Icc}(a, b) = \{x \in \alpha \mid a \leq x \leq b\}$.
Finset.coe_Ico theorem
(a b : α) : (Ico a b : Set α) = Set.Ico a b
Full source 
@[simp, norm_cast]
theorem coe_Ico (a b : α) : (Ico a b : Set α) = Set.Ico a b :=
  Set.ext fun _ => mem_Ico
Equality of Finset and Set Closed-Open Intervals: $\text{Ico}(a, b) = [a, b)$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the underlying set of the closed-open interval finset $\text{Ico}(a, b)$ is equal to the set-theoretic closed-open interval $\text{Ico}(a, b) = \{x \in \alpha \mid a \leq x < b\}$.
Finset.coe_Ioc theorem
(a b : α) : (Ioc a b : Set α) = Set.Ioc a b
Full source 
@[simp, norm_cast]
theorem coe_Ioc (a b : α) : (Ioc a b : Set α) = Set.Ioc a b :=
  Set.ext fun _ => mem_Ioc
Equality of Finset and Set Open-Closed Intervals: $\text{Ioc}(a, b) = (a, b]$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the underlying set of the open-closed interval finset $\text{Ioc}(a, b)$ is equal to the set-theoretic open-closed interval $(a, b] = \{x \in \alpha \mid a < x \leq b\}$.
Finset.coe_Ioo theorem
(a b : α) : (Ioo a b : Set α) = Set.Ioo a b
Full source 
@[simp, norm_cast]
theorem coe_Ioo (a b : α) : (Ioo a b : Set α) = Set.Ioo a b :=
  Set.ext fun _ => mem_Ioo
Equality of Finset and Set Open Intervals: $\text{Ioo}(a, b) = (a, b)$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the underlying set of the open interval finset $\text{Ioo}(a, b)$ is equal to the set-theoretic open interval $(a, b) = \{x \in \alpha \mid a < x < b\}$.
Fintype.card_Icc theorem
(a b : α) [Fintype (Set.Icc a b)] : Fintype.card (Set.Icc a b) = #(Icc a b)
Full source 
@[simp]
theorem _root_.Fintype.card_Icc (a b : α) [Fintype (Set.Icc a b)] :
    Fintype.card (Set.Icc a b) = #(Icc a b) :=
  Fintype.card_of_finset' _ fun _ ↦ by simp
Cardinality of Closed Interval Equals Size of Finset Representation
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the cardinality of the closed interval $[a, b]$ as a set is equal to the size of the corresponding finset $\text{Icc}(a, b)$.
Fintype.card_Ico theorem
(a b : α) [Fintype (Set.Ico a b)] : Fintype.card (Set.Ico a b) = #(Ico a b)
Full source 
@[simp]
theorem _root_.Fintype.card_Ico (a b : α) [Fintype (Set.Ico a b)] :
    Fintype.card (Set.Ico a b) = #(Ico a b) :=
  Fintype.card_of_finset' _ fun _ ↦ by simp
Cardinality of Half-Open Interval Equals Finset Size in Locally Finite Order
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the cardinality of the half-open interval $[a, b)$ as a set is equal to the size of its representation as a finset, i.e., $|\text{Ico}(a, b)| = \#(\text{Ico}(a, b))$.
Fintype.card_Ioc theorem
(a b : α) [Fintype (Set.Ioc a b)] : Fintype.card (Set.Ioc a b) = #(Ioc a b)
Full source 
@[simp]
theorem _root_.Fintype.card_Ioc (a b : α) [Fintype (Set.Ioc a b)] :
    Fintype.card (Set.Ioc a b) = #(Ioc a b) :=
  Fintype.card_of_finset' _ fun _ ↦ by simp
Cardinality of Open-Closed Interval Equals Finset Size in Locally Finite Order
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the cardinality of the set $\text{Ioc}(a, b) = \{x \in \alpha \mid a < x \leq b\}$ is equal to the size of the corresponding finset $\text{Ioc}(a, b)$, i.e., $|\text{Ioc}(a, b)| = \#(\text{Ioc}(a, b))$.
Fintype.card_Ioo theorem
(a b : α) [Fintype (Set.Ioo a b)] : Fintype.card (Set.Ioo a b) = #(Ioo a b)
Full source 
@[simp]
theorem _root_.Fintype.card_Ioo (a b : α) [Fintype (Set.Ioo a b)] :
    Fintype.card (Set.Ioo a b) = #(Ioo a b) :=
  Fintype.card_of_finset' _ fun _ ↦ by simp
Cardinality of Open Interval in Locally Finite Order Equals Finset Size
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the cardinality of the open interval $(a, b)$ as a set is equal to the size of its representation as a finset, i.e., $|\text{Ioo}(a, b)| = \#(\text{Ioo}(a, b))$.
Finset.Ici definition
(a : α) : Finset α
Full source 
/-- The finset $[a, ∞)$ of elements `x` such that `a ≤ x`. Basically `Set.Ici a` as a finset. -/
def Ici (a : α) : Finset α :=
  LocallyFiniteOrderTop.finsetIci a
Closed-infinite interval as a finset
Informal description
For an element $a$ in a locally finite order with finite intervals bounded below, the finset $\text{Ici}(a)$ consists of all elements $x$ such that $a \leq x$. This is the finset representation of the set $\{x \mid a \leq x\}$.
Finset.Ioi definition
(a : α) : Finset α
Full source 
/-- The finset $(a, ∞)$ of elements `x` such that `a < x`. Basically `Set.Ioi a` as a finset. -/
def Ioi (a : α) : Finset α :=
  LocallyFiniteOrderTop.finsetIoi a
Open infinite interval as a finset
Informal description
For an element $a$ in a locally finite order with finite intervals bounded below, the finset $\text{Ioi}(a)$ consists of all elements $x$ such that $a < x$. This is the finset representation of the open interval $(a, \infty)$.
Finset.mem_Ici theorem
: x ∈ Ici a ↔ a ≤ x
Full source 
@[simp]
theorem mem_Ici : x ∈ Ici ax ∈ Ici a ↔ a ≤ x :=
  LocallyFiniteOrderTop.finset_mem_Ici _ _
Membership in Closed-Infinite Interval
Informal description
For any element $x$ in a locally finite order with finite intervals bounded below, $x$ belongs to the closed-infinite interval $\text{Ici}(a)$ if and only if $a \leq x$.
Finset.mem_Ioi theorem
: x ∈ Ioi a ↔ a < x
Full source 
@[simp]
theorem mem_Ioi : x ∈ Ioi ax ∈ Ioi a ↔ a < x :=
  LocallyFiniteOrderTop.finset_mem_Ioi _ _
Membership in Open-Infinite Interval: $x \in \text{Ioi}(a) \leftrightarrow a < x$
Informal description
For any elements $x$ and $a$ in a locally finite order with finite intervals bounded below, $x$ belongs to the open-infinite interval $\text{Ioi}(a)$ if and only if $a < x$.
Finset.coe_Ici theorem
(a : α) : (Ici a : Set α) = Set.Ici a
Full source 
@[simp, norm_cast]
theorem coe_Ici (a : α) : (Ici a : Set α) = Set.Ici a :=
  Set.ext fun _ => mem_Ici
Equality of Finset and Set Representations for Closed-Infinite Interval
Informal description
For any element $a$ in a locally finite order with finite intervals bounded below, the underlying set of the finset $\text{Ici}(a)$ is equal to the set $\text{Ici}(a) = \{x \mid a \leq x\}$.
Finset.coe_Ioi theorem
(a : α) : (Ioi a : Set α) = Set.Ioi a
Full source 
@[simp, norm_cast]
theorem coe_Ioi (a : α) : (Ioi a : Set α) = Set.Ioi a :=
  Set.ext fun _ => mem_Ioi
Equality of Finset and Set Representations for Open-Infinite Interval
Informal description
For any element $a$ in a locally finite order with finite intervals bounded below, the underlying set of the finset $\text{Ioi}(a)$ is equal to the set $\text{Ioi}(a) = \{x \mid a < x\}$.
Fintype.card_Ici theorem
(a : α) [Fintype (Set.Ici a)] : Fintype.card (Set.Ici a) = #(Ici a)
Full source 
@[simp]
theorem _root_.Fintype.card_Ici (a : α) [Fintype (Set.Ici a)] :
    Fintype.card (Set.Ici a) = #(Ici a) :=
  Fintype.card_of_finset' _ fun _ ↦ by simp
Cardinality Equality for Closed-Infinite Interval as Finset and Set
Informal description
For any element $a$ in a locally finite order with finite intervals bounded below, and assuming the set $\text{Ici}(a) = \{x \mid a \leq x\}$ is finite, the cardinality of $\text{Ici}(a)$ as a set is equal to the cardinality of $\text{Ici}(a)$ as a finset.
Fintype.card_Ioi theorem
(a : α) [Fintype (Set.Ioi a)] : Fintype.card (Set.Ioi a) = #(Ioi a)
Full source 
@[simp]
theorem _root_.Fintype.card_Ioi (a : α) [Fintype (Set.Ioi a)] :
    Fintype.card (Set.Ioi a) = #(Ioi a) :=
  Fintype.card_of_finset' _ fun _ ↦ by simp
Cardinality Equality for Open-Infinite Interval as Finset and Set
Informal description
For any element $a$ in a locally finite order with finite intervals bounded below, and assuming the set $\text{Ioi}(a) = \{x \mid a < x\}$ is finite, the cardinality of $\text{Ioi}(a)$ as a set is equal to the cardinality of $\text{Ioi}(a)$ as a finset.
Finset.Iic definition
(b : α) : Finset α
Full source 
/-- The finset $(-∞, b]$ of elements `x` such that `x ≤ b`. Basically `Set.Iic b` as a finset. -/
def Iic (b : α) : Finset α :=
  LocallyFiniteOrderBot.finsetIic b
Lower-closed interval as a finset
Informal description
For an element $b$ in a locally finite order with finite lower-bounded intervals, the finset $\text{Iic}(b)$ consists of all elements $x$ such that $x \leq b$. This is the finset version of the set $\{x \mid x \leq b\}$.
Finset.Iio definition
(b : α) : Finset α
Full source 
/-- The finset $(-∞, b)$ of elements `x` such that `x < b`. Basically `Set.Iio b` as a finset. -/
def Iio (b : α) : Finset α :=
  LocallyFiniteOrderBot.finsetIio b
Open lower interval as a finset
Informal description
For an element $b$ in a locally finite order with finite lower-bounded intervals, the finset $\text{Iio}(b)$ consists of all elements $x$ such that $x < b$. This is the finset version of the set $\{x \mid x < b\}$.
Finset.mem_Iic theorem
: x ∈ Iic a ↔ x ≤ a
Full source 
@[simp]
theorem mem_Iic : x ∈ Iic ax ∈ Iic a ↔ x ≤ a :=
  LocallyFiniteOrderBot.finset_mem_Iic _ _
Membership in Closed Lower Interval Finset: $x \in \text{Iic}(a) \leftrightarrow x \leq a$
Informal description
For any elements $x$ and $a$ in a locally finite order with finite lower-bounded intervals, $x$ belongs to the finset $\text{Iic}(a)$ if and only if $x \leq a$.
Finset.mem_Iio theorem
: x ∈ Iio a ↔ x < a
Full source 
@[simp]
theorem mem_Iio : x ∈ Iio ax ∈ Iio a ↔ x < a :=
  LocallyFiniteOrderBot.finset_mem_Iio _ _
Membership in Open Lower Interval Finset: $x \in \text{Iio}(a) \leftrightarrow x < a$
Informal description
For any elements $x$ and $a$ in a locally finite order with finite lower-bounded intervals, $x$ belongs to the finset $\text{Iio}(a)$ if and only if $x < a$.
Finset.coe_Iic theorem
(a : α) : (Iic a : Set α) = Set.Iic a
Full source 
@[simp, norm_cast]
theorem coe_Iic (a : α) : (Iic a : Set α) = Set.Iic a :=
  Set.ext fun _ => mem_Iic
Equality of Finset and Set Representations for Closed Lower Interval: $\operatorname{Iic}(a) = \{x \mid x \leq a\}$
Informal description
For any element $a$ in a locally finite order with finite lower-bounded intervals, the underlying set of the finset $\operatorname{Iic}(a)$ is equal to the set $\{x \mid x \leq a\}$.
Finset.coe_Iio theorem
(a : α) : (Iio a : Set α) = Set.Iio a
Full source 
@[simp, norm_cast]
theorem coe_Iio (a : α) : (Iio a : Set α) = Set.Iio a :=
  Set.ext fun _ => mem_Iio
Equality of Finset and Set Representations for Open Lower Interval: $\operatorname{Iio}(a) = \{x \mid x < a\}$
Informal description
For any element $a$ in a locally finite order with finite lower-bounded intervals, the underlying set of the finset $\operatorname{Iio}(a)$ is equal to the set $\{x \mid x < a\}$.
Fintype.card_Iic theorem
(a : α) [Fintype (Set.Iic a)] : Fintype.card (Set.Iic a) = #(Iic a)
Full source 
@[simp]
theorem _root_.Fintype.card_Iic (a : α) [Fintype (Set.Iic a)] :
    Fintype.card (Set.Iic a) = #(Iic a) :=
  Fintype.card_of_finset' _ fun _ ↦ by simp
Cardinality of Closed Lower Interval as Finset and Set
Informal description
For any element $a$ in a locally finite order with finite lower-bounded intervals, if the set $\operatorname{Iic}(a) = \{x \mid x \leq a\}$ is finite (i.e., has a `Fintype` instance), then the cardinality of this set equals the size of the finset $\operatorname{Iic}(a)$.
Fintype.card_Iio theorem
(a : α) [Fintype (Set.Iio a)] : Fintype.card (Set.Iio a) = #(Iio a)
Full source 
@[simp]
theorem _root_.Fintype.card_Iio (a : α) [Fintype (Set.Iio a)] :
    Fintype.card (Set.Iio a) = #(Iio a) :=
  Fintype.card_of_finset' _ fun _ ↦ by simp
Cardinality of Open Lower Interval as Finset and Set
Informal description
For any element $a$ in a locally finite order with finite lower-bounded intervals, if the set $\operatorname{Iio}(a) = \{x \mid x < a\}$ is finite (i.e., has a `Fintype` instance), then the cardinality of this set equals the size of the finset $\operatorname{Iio}(a)$.
LocallyFiniteOrder.toLocallyFiniteOrderTop instance
: LocallyFiniteOrderTop α
Full source 
instance (priority := 100) _root_.LocallyFiniteOrder.toLocallyFiniteOrderTop :
    LocallyFiniteOrderTop α where
  finsetIci b := Icc b ⊤
  finsetIoi b := Ioc b ⊤
  finset_mem_Ici a x := by rw [mem_Icc, and_iff_left le_top]
  finset_mem_Ioi a x := by rw [mem_Ioc, and_iff_left le_top]
Locally Finite Order with Top Element Preserves Finite Intervals Bounded Below
Informal description
Every locally finite order $\alpha$ with a top element $\top$ is also a locally finite order where all intervals bounded below are finite. In particular, for any element $a \in \alpha$, the intervals $\operatorname{Ici}(a) = [a, \top]$ and $\operatorname{Ioi}(a) = (a, \top]$ can be represented as finite sets.
Finset.Ici_eq_Icc theorem
(a : α) : Ici a = Icc a ⊤
Full source 
theorem Ici_eq_Icc (a : α) : Ici a = Icc a ⊤ :=
  rfl
Closed-Infinite Interval Equals Closed Interval to Top
Informal description
For any element $a$ in a locally finite order $\alpha$ with a top element $\top$, the closed-infinite interval $\operatorname{Ici}(a) = \{x \mid a \leq x\}$ is equal to the closed interval $\operatorname{Icc}(a, \top) = \{x \mid a \leq x \leq \top\}$.
Finset.Ioi_eq_Ioc theorem
(a : α) : Ioi a = Ioc a ⊤
Full source 
theorem Ioi_eq_Ioc (a : α) : Ioi a = Ioc a ⊤ :=
  rfl
Equality of Open-Infinite and Open-Closed Intervals in Locally Finite Orders with Top Element
Informal description
For any element $a$ in a locally finite order $\alpha$ with a top element $\top$, the open-infinite interval $\operatorname{Ioi}(a) = \{x \mid a < x\}$ is equal to the open-closed interval $\operatorname{Ioc}(a, \top) = \{x \mid a < x \leq \top\}$.
Finset.LocallyFiniteOrder.toLocallyFiniteOrderBot instance
: LocallyFiniteOrderBot α
Full source 
instance (priority := 100) LocallyFiniteOrder.toLocallyFiniteOrderBot :
    LocallyFiniteOrderBot α where
  finsetIic := Icc ⊥
  finsetIio := Ico ⊥
  finset_mem_Iic a x := by rw [mem_Icc, and_iff_right bot_le]
  finset_mem_Iio a x := by rw [mem_Ico, and_iff_right bot_le]
Locally Finite Order with Bottom Element Implies Finite Lower-Bounded Intervals
Informal description
Every locally finite order with a bottom element is also a locally finite order where all lower-bounded intervals are finite. This means that for any element $a$ in the order $\alpha$, the intervals $(-\infty, a]$ and $(-\infty, a)$ can be represented as finite sets.
Finset.Iic_eq_Icc theorem
: Iic = Icc (⊥ : α)
Full source 
theorem Iic_eq_Icc : Iic = Icc (⊥ : α) :=
  rfl
Equality of Lower-Closed and Bottom-Closed Intervals in Locally Finite Orders with Bottom Element
Informal description
For any element $b$ in a locally finite order $\alpha$ with a bottom element $\bot$, the lower-closed interval $\text{Iic}(b)$ is equal to the closed interval $\text{Icc}(\bot, b)$. That is, the set of all elements $x \in \alpha$ such that $x \leq b$ is equal to the set of all elements $x \in \alpha$ such that $\bot \leq x \leq b$.
Finset.Iio_eq_Ico theorem
: Iio = Ico (⊥ : α)
Full source 
theorem Iio_eq_Ico : Iio = Ico (⊥ : α) :=
  rfl
Equality of Open Lower Interval and Half-Open Interval from Bottom in Locally Finite Orders with Bottom Element
Informal description
For any element $b$ in a locally finite order $\alpha$ with a bottom element $\bot$, the open lower interval $\text{Iio}(b)$ is equal to the half-open interval $\text{Ico}(\bot, b)$. That is, the set of all elements $x \in \alpha$ such that $x < b$ is equal to the set of all elements $x \in \alpha$ such that $\bot \leq x < b$.
Finset.uIcc definition
(a b : α) : Finset α
Full source 
/-- `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. -/
def uIcc (a b : α) : Finset α :=
  Icc (a ⊓ b) (a ⊔ b)
Unordered closed interval as a finset
Informal description
For elements \( a \) and \( b \) in a lattice \(\alpha\), the finset \(\text{uIcc}(a, b)\) consists of all elements lying between the infimum \( a \sqcap b \) and the supremum \( a \sqcup b \), inclusive. In a product type, this corresponds to the bounding box of the two elements.
FinsetInterval.term[[_,_]] definition
: Lean.ParserDescr✝
Full source 
@[inherit_doc]
scoped[FinsetInterval] notation "[[" a ", " b "]]" => Finset.uIcc a b
Notation for unordered closed interval as finset
Informal description
The notation `[[a, b]]` represents the unordered closed interval between elements `a` and `b` in a locally finite order, implemented as a finset. This is equivalent to `Finset.uIcc a b`, which contains all elements between `a` and `b` regardless of their order (i.e., it equals `[a, b]` if `a ≤ b` or `[b, a]` if `b ≤ a`).
Finset.mem_uIcc theorem
: x ∈ uIcc a b ↔ a ⊓ b ≤ x ∧ x ≤ a ⊔ b
Full source 
@[simp]
theorem mem_uIcc : x ∈ uIcc a bx ∈ uIcc a b ↔ a ⊓ b ≤ x ∧ x ≤ a ⊔ b :=
  mem_Icc
Membership Criterion for Unordered Closed Interval Finset
Informal description
For any elements $x, a, b$ in a lattice $\alpha$, the element $x$ belongs to the unordered closed interval finset $\text{uIcc}(a, b)$ if and only if $x$ lies between the infimum $a \sqcap b$ and the supremum $a \sqcup b$, i.e., $a \sqcap b \leq x \leq a \sqcup b$.
Finset.coe_uIcc theorem
(a b : α) : (Finset.uIcc a b : Set α) = Set.uIcc a b
Full source 
@[simp, norm_cast]
theorem coe_uIcc (a b : α) : (Finset.uIcc a b : Set α) = Set.uIcc a b :=
  coe_Icc _ _
Equality of Finset and Set Unordered Closed Intervals: $\text{uIcc}(a, b) = [a \sqcap b, a \sqcup b]$
Informal description
For any elements $a$ and $b$ in a lattice $\alpha$, the underlying set of the unordered closed interval finset $\text{uIcc}(a, b)$ is equal to the set-theoretic unordered closed interval $\text{uIcc}(a, b) = [a \sqcap b, a \sqcup b]$.
Fintype.card_uIcc theorem
(a b : α) [Fintype (Set.uIcc a b)] : Fintype.card (Set.uIcc a b) = #(uIcc a b)
Full source 
@[simp]
theorem _root_.Fintype.card_uIcc (a b : α) [Fintype (Set.uIcc a b)] :
    Fintype.card (Set.uIcc a b) = #(uIcc a b) :=
  Fintype.card_of_finset' _ fun _ ↦ by simp [Set.uIcc]
Cardinality of Unordered Closed Interval Equals Finset Size
Informal description
For any elements $a$ and $b$ in a lattice $\alpha$ where the unordered closed interval $[a \sqcap b, a \sqcup b]$ is finite, the cardinality of the set $\text{uIcc}(a, b)$ is equal to the size of the finset $\text{uIcc}(a, b)$.
Mathlib.Meta.elabFinsetBuilderIxx definition
: TermElab
Full source 
/-- Elaborate set builder notation for `Finset`.

* `{x ≤ a | p x}` is elaborated as `Finset.filter (fun x ↦ p x) (Finset.Iic a)` if the expected type
  is `Finset ?α`.
* `{x ≥ a | p x}` is elaborated as `Finset.filter (fun x ↦ p x) (Finset.Ici a)` if the expected type
  is `Finset ?α`.
* `{x < a | p x}` is elaborated as `Finset.filter (fun x ↦ p x) (Finset.Iio a)` if the expected type
  is `Finset ?α`.
* `{x > a | p x}` is elaborated as `Finset.filter (fun x ↦ p x) (Finset.Ioi a)` if the expected type
  is `Finset ?α`.

See also
* `Data.Set.Defs` for the `Set` builder notation elaborator that this elaborator partly overrides.
* `Data.Finset.Basic` for the `Finset` builder notation elaborator partly overriding this one for
  syntax of the form `{x ∈ s | p x}`.
* `Data.Fintype.Basic` for the `Finset` builder notation elaborator handling syntax of the form
  `{x | p x}`, `{x : α | p x}`, `{x ∉ s | p x}`, `{x ≠ a | p x}`.

TODO: Write a delaborator
-/
@[term_elab setBuilder]
def elabFinsetBuilderIxx : TermElab
  | `({ $x:ident ≤ $a | $p }), expectedType? => do
    -- If the expected type is not known to be `Finset ?α`, give up.
    unless ← knownToBeFinsetNotSet expectedType? do throwUnsupportedSyntax
    elabTerm (← `(Finset.filter (fun $x:ident ↦ $p) (Finset.Iic $a))) expectedType?
  | `({ $x:ident ≥ $a | $p }), expectedType? => do
    -- If the expected type is not known to be `Finset ?α`, give up.
    unless ← knownToBeFinsetNotSet expectedType? do throwUnsupportedSyntax
    elabTerm (← `(Finset.filter (fun $x:ident ↦ $p) (Finset.Ici $a))) expectedType?
  | `({ $x:ident < $a | $p }), expectedType? => do
    -- If the expected type is not known to be `Finset ?α`, give up.
    unless ← knownToBeFinsetNotSet expectedType? do throwUnsupportedSyntax
    elabTerm (← `(Finset.filter (fun $x:ident ↦ $p) (Finset.Iio $a))) expectedType?
  | `({ $x:ident > $a | $p }), expectedType? => do
    -- If the expected type is not known to be `Finset ?α`, give up.
    unless ← knownToBeFinsetNotSet expectedType? do throwUnsupportedSyntax
    elabTerm (← `(Finset.filter (fun $x:ident ↦ $p) (Finset.Ioi $a))) expectedType?
  | _, _ => throwUnsupportedSyntax
Finset builder notation elaborator for interval-bounded sets
Informal description
The elaborator for finset builder notation with interval bounds. Given a pattern `{x ≤ a | p x}`, it elaborates to `Finset.filter (fun x ↦ p x) (Finset.Iic a)` when the expected type is known to be a finset. Similarly handles patterns with `≥`, `<`, and `>` by using the appropriate interval constructors `Ici`, `Iio`, and `Ioi` respectively.
Set.instFintypeIcc instance
: Fintype (Icc a b)
Full source 
instance instFintypeIcc : Fintype (Icc a b) := .ofFinset (Finset.Icc a b) fun _ => Finset.mem_Icc
Finiteness of Closed Intervals in Locally Finite Orders
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the closed interval $[a, b]$ is finite and can be represented as a finset.
Set.instFintypeIco instance
: Fintype (Ico a b)
Full source 
instance instFintypeIco : Fintype (Ico a b) := .ofFinset (Finset.Ico a b) fun _ => Finset.mem_Ico
Finiteness of Closed-Open Intervals in Locally Finite Orders
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the closed-open interval $[a, b)$ is finite and can be represented as a finset.
Set.instFintypeIoc instance
: Fintype (Ioc a b)
Full source 
instance instFintypeIoc : Fintype (Ioc a b) := .ofFinset (Finset.Ioc a b) fun _ => Finset.mem_Ioc
Finiteness of Open-Closed Intervals in Locally Finite Orders
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the open-closed interval $(a, b]$ is finite and can be represented as a finset.
Set.instFintypeIoo instance
: Fintype (Ioo a b)
Full source 
instance instFintypeIoo : Fintype (Ioo a b) := .ofFinset (Finset.Ioo a b) fun _ => Finset.mem_Ioo
Finiteness of Open Intervals in Locally Finite Orders
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the open interval $(a, b)$ is finite and can be represented as a finset.
Set.finite_Icc theorem
: (Icc a b).Finite
Full source 
theorem finite_Icc : (Icc a b).Finite :=
  (Icc a b).toFinite
Finiteness of Closed Intervals in Locally Finite Orders
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the closed interval $[a, b] = \{x \in \alpha \mid a \leq x \leq b\}$ is finite.
Set.finite_Ico theorem
: (Ico a b).Finite
Full source 
theorem finite_Ico : (Ico a b).Finite :=
  (Ico a b).toFinite
Finiteness of Closed-Open Intervals in Locally Finite Orders
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the closed-open interval $[a, b)$ is finite.
Set.finite_Ioc theorem
: (Ioc a b).Finite
Full source 
theorem finite_Ioc : (Ioc a b).Finite :=
  (Ioc a b).toFinite
Finiteness of open-closed intervals in locally finite orders
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the open-closed interval $(a, b]$ is finite.
Set.finite_Ioo theorem
: (Ioo a b).Finite
Full source 
theorem finite_Ioo : (Ioo a b).Finite :=
  (Ioo a b).toFinite
Finiteness of Open Intervals in Locally Finite Orders
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the open interval $(a, b) = \{x \in \alpha \mid a < x < b\}$ is finite.
Set.instFintypeIci instance
: Fintype (Ici a)
Full source 
instance instFintypeIci : Fintype (Ici a) := .ofFinset (Finset.Ici a) fun _ => Finset.mem_Ici
Finiteness of Closed-Infinite Intervals in Locally Finite Orders
Informal description
For any element $a$ in a locally finite order with finite intervals bounded below, the left-closed right-infinite interval $[a, \infty)$ can be given a fintype structure.
Set.instFintypeIoi instance
: Fintype (Ioi a)
Full source 
instance instFintypeIoi : Fintype (Ioi a) := .ofFinset (Finset.Ioi a) fun _ => Finset.mem_Ioi
Finiteness of Open-Infinite Intervals in Locally Finite Orders
Informal description
For any element $a$ in a locally finite order with finite intervals bounded below, the open-infinite interval $(a, \infty)$ can be given a fintype structure.
Set.finite_Ici theorem
: (Ici a).Finite
Full source 
theorem finite_Ici : (Ici a).Finite :=
  (Ici a).toFinite
Finiteness of Closed-Infinite Intervals in Locally Finite Orders
Informal description
For any element $a$ in a locally finite order with finite intervals bounded below, the left-closed right-infinite interval $[a, \infty)$ is finite.
Set.finite_Ioi theorem
: (Ioi a).Finite
Full source 
theorem finite_Ioi : (Ioi a).Finite :=
  (Ioi a).toFinite
Finiteness of Open-Infinite Intervals in Locally Finite Orders
Informal description
For any element $a$ in a locally finite order with finite intervals bounded below, the open-infinite interval $(a, \infty)$ is finite.
Set.instFintypeIic instance
: Fintype (Iic b)
Full source 
instance instFintypeIic : Fintype (Iic b) := .ofFinset (Finset.Iic b) fun _ => Finset.mem_Iic
Finiteness of Closed Lower Intervals in Locally Finite Orders
Informal description
For any element $b$ in a locally finite order with finite lower-bounded intervals, the closed lower interval $\text{Iic}(b) = \{x \mid x \leq b\}$ is finite and can be represented as a finset.
Set.instFintypeIio instance
: Fintype (Iio b)
Full source 
instance instFintypeIio : Fintype (Iio b) := .ofFinset (Finset.Iio b) fun _ => Finset.mem_Iio
Finiteness of Open Lower Intervals in Locally Finite Orders
Informal description
For any element $b$ in a locally finite order with finite lower-bounded intervals, the open lower interval $\operatorname{Iio}(b) = \{x \mid x < b\}$ is finite and can be represented as a finset.
Set.finite_Iic theorem
: (Iic b).Finite
Full source 
theorem finite_Iic : (Iic b).Finite :=
  (Iic b).toFinite
Finiteness of Closed Lower Intervals in Locally Finite Orders
Informal description
For any element $b$ in a locally finite order with finite lower-bounded intervals, the closed lower interval $\text{Iic}(b) = \{x \mid x \leq b\}$ is finite.
Set.finite_Iio theorem
: (Iio b).Finite
Full source 
theorem finite_Iio : (Iio b).Finite :=
  (Iio b).toFinite
Finiteness of Open Lower Intervals in Locally Finite Orders
Informal description
For any element $b$ in a preorder $\alpha$ that is a locally finite order with finite lower-bounded intervals, the open lower interval $\operatorname{Iio}(b) = \{x \mid x < b\}$ is finite.
Set.fintypeUIcc instance
: Fintype (uIcc a b)
Full source 
instance fintypeUIcc : Fintype (uIcc a b) :=
  Fintype.ofFinset (Finset.uIcc a b) fun _ => Finset.mem_uIcc
Finiteness of Unordered Closed Intervals in a Lattice
Informal description
For any two elements $a$ and $b$ in a lattice $\alpha$, the unordered closed interval $\text{uIcc}(a, b) = [a \sqcap b, a \sqcup b]$ is finite and can be represented as a fintype.
Set.finite_interval theorem
: (uIcc a b).Finite
Full source 
@[simp]
theorem finite_interval : (uIcc a b).Finite := (uIcc _ _).toFinite
Finiteness of Unordered Closed Intervals in a Lattice
Informal description
For any two elements $a$ and $b$ in a lattice $\alpha$, the unordered closed interval $\text{uIcc}(a, b) = [a \sqcap b, a \sqcup b]$ is finite.
LocallyFiniteOrder.ofFiniteIcc definition
(h : ∀ a b : α, (Set.Icc a b).Finite) : LocallyFiniteOrder α
Full source 
/-- A noncomputable constructor from the finiteness of all closed intervals. -/
noncomputable def LocallyFiniteOrder.ofFiniteIcc (h : ∀ a b : α, (Set.Icc a b).Finite) :
    LocallyFiniteOrder α :=
  @LocallyFiniteOrder.ofIcc' α _ (Classical.decRel _) (fun a b => (h a b).toFinset) fun a b x => by
    rw [Set.Finite.mem_toFinset, Set.mem_Icc]
Locally finite order from finite closed intervals
Informal description
Given a preorder $\alpha$ such that for any two elements $a, b \in \alpha$, the closed interval $[a, b] = \{x \in \alpha \mid a \leq x \leq b\}$ is finite, this constructs a locally finite order structure on $\alpha$. The construction is noncomputable and uses the finiteness of all closed intervals to define the required finite sets for other interval types (open-closed, closed-open, and open-open intervals).
Fintype.toLocallyFiniteOrder abbrev
[Fintype α] [DecidableLT α] [DecidableLE α] : LocallyFiniteOrder α
Full source 
/-- A fintype is a locally finite order.

This is not an instance as it would not be defeq to better instances such as
`Fin.locallyFiniteOrder`.
-/
abbrev Fintype.toLocallyFiniteOrder [Fintype α] [DecidableLT α] [DecidableLE α] :
    LocallyFiniteOrder α where
  finsetIcc a b := (Set.Icc a b).toFinset
  finsetIco a b := (Set.Ico a b).toFinset
  finsetIoc a b := (Set.Ioc a b).toFinset
  finsetIoo a b := (Set.Ioo a b).toFinset
  finset_mem_Icc a b x := by simp only [Set.mem_toFinset, Set.mem_Icc]
  finset_mem_Ico a b x := by simp only [Set.mem_toFinset, Set.mem_Ico]
  finset_mem_Ioc a b x := by simp only [Set.mem_toFinset, Set.mem_Ioc]
  finset_mem_Ioo a b x := by simp only [Set.mem_toFinset, Set.mem_Ioo]
Finite Types as Locally Finite Orders
Informal description
For any finite type $\alpha$ with decidable strict order and decidable non-strict order relations, there exists a locally finite order structure on $\alpha$ where all bounded intervals are finite.
instSubsingletonLocallyFiniteOrder instance
: Subsingleton (LocallyFiniteOrder α)
Full source 
instance : Subsingleton (LocallyFiniteOrder α) :=
  Subsingleton.intro fun h₀ h₁ => by
    obtain ⟨h₀_finset_Icc, h₀_finset_Ico, h₀_finset_Ioc, h₀_finset_Ioo,
      h₀_finset_mem_Icc, h₀_finset_mem_Ico, h₀_finset_mem_Ioc, h₀_finset_mem_Ioo⟩ := h₀
    obtain ⟨h₁_finset_Icc, h₁_finset_Ico, h₁_finset_Ioc, h₁_finset_Ioo,
      h₁_finset_mem_Icc, h₁_finset_mem_Ico, h₁_finset_mem_Ioc, h₁_finset_mem_Ioo⟩ := h₁
    have hIcc : h₀_finset_Icc = h₁_finset_Icc := by
      ext a b x
      rw [h₀_finset_mem_Icc, h₁_finset_mem_Icc]
    have hIco : h₀_finset_Ico = h₁_finset_Ico := by
      ext a b x
      rw [h₀_finset_mem_Ico, h₁_finset_mem_Ico]
    have hIoc : h₀_finset_Ioc = h₁_finset_Ioc := by
      ext a b x
      rw [h₀_finset_mem_Ioc, h₁_finset_mem_Ioc]
    have hIoo : h₀_finset_Ioo = h₁_finset_Ioo := by
      ext a b x
      rw [h₀_finset_mem_Ioo, h₁_finset_mem_Ioo]
    simp_rw [hIcc, hIco, hIoc, hIoo]
Uniqueness of Locally Finite Order Structure
Informal description
For any preorder $\alpha$, there is at most one instance of a locally finite order structure on $\alpha$.
instSubsingletonLocallyFiniteOrderTop instance
: Subsingleton (LocallyFiniteOrderTop α)
Full source 
instance : Subsingleton (LocallyFiniteOrderTop α) :=
  Subsingleton.intro fun h₀ h₁ => by
    obtain ⟨h₀_finset_Ioi, h₀_finset_Ici, h₀_finset_mem_Ici, h₀_finset_mem_Ioi⟩ := h₀
    obtain ⟨h₁_finset_Ioi, h₁_finset_Ici, h₁_finset_mem_Ici, h₁_finset_mem_Ioi⟩ := h₁
    have hIci : h₀_finset_Ici = h₁_finset_Ici := by
      ext a b
      rw [h₀_finset_mem_Ici, h₁_finset_mem_Ici]
    have hIoi : h₀_finset_Ioi = h₁_finset_Ioi := by
      ext a b
      rw [h₀_finset_mem_Ioi, h₁_finset_mem_Ioi]
    simp_rw [hIci, hIoi]
Uniqueness of Locally Finite Order with Finite Upper-Bounded Intervals
Informal description
For any preorder $\alpha$, there is at most one instance of `LocallyFiniteOrderTop` on $\alpha$.
instSubsingletonLocallyFiniteOrderBot instance
: Subsingleton (LocallyFiniteOrderBot α)
Full source 
instance : Subsingleton (LocallyFiniteOrderBot α) :=
  Subsingleton.intro fun h₀ h₁ => by
    obtain ⟨h₀_finset_Iio, h₀_finset_Iic, h₀_finset_mem_Iic, h₀_finset_mem_Iio⟩ := h₀
    obtain ⟨h₁_finset_Iio, h₁_finset_Iic, h₁_finset_mem_Iic, h₁_finset_mem_Iio⟩ := h₁
    have hIic : h₀_finset_Iic = h₁_finset_Iic := by
      ext a b
      rw [h₀_finset_mem_Iic, h₁_finset_mem_Iic]
    have hIio : h₀_finset_Iio = h₁_finset_Iio := by
      ext a b
      rw [h₀_finset_mem_Iio, h₁_finset_mem_Iio]
    simp_rw [hIic, hIio]
Uniqueness of Locally Finite Order with Finite Lower-Bounded Intervals
Informal description
For any preorder $\alpha$, there is at most one instance of `LocallyFiniteOrderBot` on $\alpha$.
OrderEmbedding.locallyFiniteOrder definition
[LocallyFiniteOrder β] (f : α ↪o β) : LocallyFiniteOrder α
Full source 
/-- Given an order embedding `α ↪o β`, pulls back the `LocallyFiniteOrder` on `β` to `α`. -/
protected noncomputable def OrderEmbedding.locallyFiniteOrder [LocallyFiniteOrder β] (f : α ↪o β) :
    LocallyFiniteOrder α where
  finsetIcc a b := (Icc (f a) (f b)).preimage f f.toEmbedding.injective.injOn
  finsetIco a b := (Ico (f a) (f b)).preimage f f.toEmbedding.injective.injOn
  finsetIoc a b := (Ioc (f a) (f b)).preimage f f.toEmbedding.injective.injOn
  finsetIoo a b := (Ioo (f a) (f b)).preimage f f.toEmbedding.injective.injOn
  finset_mem_Icc a b x := by rw [mem_preimage, mem_Icc, f.le_iff_le, f.le_iff_le]
  finset_mem_Ico a b x := by rw [mem_preimage, mem_Ico, f.le_iff_le, f.lt_iff_lt]
  finset_mem_Ioc a b x := by rw [mem_preimage, mem_Ioc, f.lt_iff_lt, f.le_iff_le]
  finset_mem_Ioo a b x := by rw [mem_preimage, mem_Ioo, f.lt_iff_lt, f.lt_iff_lt]
Pullback of Locally Finite Order via Order Embedding
Informal description
Given a locally finite order $\beta$ and an order embedding $f \colon \alpha \hookrightarrow \beta$, this definition pulls back the locally finite order structure from $\beta$ to $\alpha$. Specifically, for any elements $a, b \in \alpha$, the intervals in $\alpha$ are defined as the preimages under $f$ of the corresponding intervals in $\beta$: - The closed interval $\text{Icc}(a, b)$ in $\alpha$ is the preimage of $\text{Icc}(f(a), f(b))$ in $\beta$. - The closed-open interval $\text{Ico}(a, b)$ in $\alpha$ is the preimage of $\text{Ico}(f(a), f(b))$ in $\beta$. - The open-closed interval $\text{Ioc}(a, b)$ in $\alpha$ is the preimage of $\text{Ioc}(f(a), f(b))$ in $\beta$. - The open interval $\text{Ioo}(a, b)$ in $\alpha$ is the preimage of $\text{Ioo}(f(a), f(b))$ in $\beta$.
OrderDual.instLocallyFiniteOrder instance
: LocallyFiniteOrder αᵒᵈ
Full source 
/-- Note we define `Icc (toDual a) (toDual b)` as `Icc α _ _ b a` (which has type `Finset α` not
`Finset αᵒᵈ`!) instead of `(Icc b a).map toDual.toEmbedding` as this means the
following is defeq:
```
lemma this : (Icc (toDual (toDual a)) (toDual (toDual b)) :) = (Icc a b :) := rfl
```
-/
instance OrderDual.instLocallyFiniteOrder : LocallyFiniteOrder αᵒᵈ where
  finsetIcc a b := @Icc α _ _ (ofDual b) (ofDual a)
  finsetIco a b := @Ioc α _ _ (ofDual b) (ofDual a)
  finsetIoc a b := @Ico α _ _ (ofDual b) (ofDual a)
  finsetIoo a b := @Ioo α _ _ (ofDual b) (ofDual a)
  finset_mem_Icc _ _ _ := (mem_Icc (α := α)).trans and_comm
  finset_mem_Ico _ _ _ := (mem_Ioc (α := α)).trans and_comm
  finset_mem_Ioc _ _ _ := (mem_Ico (α := α)).trans and_comm
  finset_mem_Ioo _ _ _ := (mem_Ioo (α := α)).trans and_comm
Locally Finite Order Dual
Informal description
The order dual $\alpha^\text{op}$ of a locally finite order $\alpha$ is also locally finite. Specifically, for any elements $a, b \in \alpha^\text{op}$, the intervals $\text{Icc}(a, b)$, $\text{Ico}(a, b)$, $\text{Ioc}(a, b)$, and $\text{Ioo}(a, b)$ in $\alpha^\text{op}$ correspond to the intervals $\text{Icc}(b, a)$, $\text{Ioc}(b, a)$, $\text{Ico}(b, a)$, and $\text{Ioo}(b, a)$ in $\alpha$, respectively, and are thus finite.
Finset.Icc_orderDual_def theorem
(a b : αᵒᵈ) : Icc a b = (Icc (ofDual b) (ofDual a)).map toDual.toEmbedding
Full source 
lemma Finset.Icc_orderDual_def (a b : αᵒᵈ) :
    Icc a b = (Icc (ofDual b) (ofDual a)).map toDual.toEmbedding := map_refl.symm
Closed Interval in Order Dual Equals Dual of Reversed Closed Interval
Informal description
For any elements $a, b$ in the order dual $\alpha^\text{op}$ of a locally finite order $\alpha$, the closed interval $\text{Icc}_{\alpha^\text{op}}(a, b)$ is equal to the image under the order dual embedding of the closed interval $\text{Icc}_\alpha(b, a)$. More precisely, $\text{Icc}_{\alpha^\text{op}}(a, b) = \text{Icc}_\alpha(\text{ofDual}(b), \text{ofDual}(a))$ mapped through the order dual embedding.
Finset.Ico_orderDual_def theorem
(a b : αᵒᵈ) : Ico a b = (Ioc (ofDual b) (ofDual a)).map toDual.toEmbedding
Full source 
lemma Finset.Ico_orderDual_def (a b : αᵒᵈ) :
    Ico a b = (Ioc (ofDual b) (ofDual a)).map toDual.toEmbedding := map_refl.symm
Closed-Open Interval in Order Dual Equals Dual of Reversed Open-Closed Interval
Informal description
For any elements $a, b$ in the order dual $\alpha^\text{op}$ of a locally finite order $\alpha$, the closed-open interval $\text{Ico}_{\alpha^\text{op}}(a, b)$ is equal to the image under the order dual embedding of the open-closed interval $\text{Ioc}_\alpha(b, a)$. More precisely, $\text{Ico}_{\alpha^\text{op}}(a, b) = \text{Ioc}_\alpha(\text{ofDual}(b), \text{ofDual}(a))$ mapped through the order dual embedding.
Finset.Ioc_orderDual_def theorem
(a b : αᵒᵈ) : Ioc a b = (Ico (ofDual b) (ofDual a)).map toDual.toEmbedding
Full source 
lemma Finset.Ioc_orderDual_def (a b : αᵒᵈ) :
    Ioc a b = (Ico (ofDual b) (ofDual a)).map toDual.toEmbedding := map_refl.symm
Open-Closed Interval in Order Dual Equals Dual of Reversed Closed-Open Interval
Informal description
For any elements $a, b$ in the order dual $\alpha^\text{op}$ of a locally finite order $\alpha$, the open-closed interval $\text{Ioc}(a, b)$ in $\alpha^\text{op}$ is equal to the image under the order dual embedding of the closed-open interval $\text{Ico}(b, a)$ in $\alpha$. More precisely, $\text{Ioc}_{\alpha^\text{op}}(a, b) = \text{Ico}_\alpha(\text{ofDual}(b), \text{ofDual}(a))$ mapped through the order dual embedding.
Finset.Ioo_orderDual_def theorem
(a b : αᵒᵈ) : Ioo a b = (Ioo (ofDual b) (ofDual a)).map toDual.toEmbedding
Full source 
lemma Finset.Ioo_orderDual_def (a b : αᵒᵈ) :
    Ioo a b = (Ioo (ofDual b) (ofDual a)).map toDual.toEmbedding := map_refl.symm
Open Interval in Order Dual Equals Dual of Reversed Open Interval
Informal description
For any elements $a, b$ in the order dual $\alpha^\text{op}$ of a locally finite order $\alpha$, the open interval $\text{Ioo}(a, b)$ in $\alpha^\text{op}$ is equal to the image under the order dual embedding of the open interval $\text{Ioo}(b, a)$ in $\alpha$. More precisely, $\text{Ioo}_{\alpha^\text{op}}(a, b) = \text{Ioo}_\alpha(\text{ofDual}(b), \text{ofDual}(a))$ mapped through the order dual embedding.
Finset.Icc_toDual theorem
: Icc (toDual a) (toDual b) = (Icc b a).map toDual.toEmbedding
Full source 
lemma Finset.Icc_toDual : Icc (toDual a) (toDual b) = (Icc b a).map toDual.toEmbedding :=
  map_refl.symm
Closed Interval in Order Dual Equals Dual of Reversed Closed Interval
Informal description
For any elements $a, b$ in a locally finite order $\alpha$, the closed interval $\text{Icc}(\text{toDual}(a), \text{toDual}(b))$ in the order dual $\alpha^\text{op}$ is equal to the image of the closed interval $\text{Icc}(b, a)$ in $\alpha$ under the order embedding $\text{toDual}$.
Finset.Ico_toDual theorem
: Ico (toDual a) (toDual b) = (Ioc b a).map toDual.toEmbedding
Full source 
lemma Finset.Ico_toDual : Ico (toDual a) (toDual b) = (Ioc b a).map toDual.toEmbedding :=
  map_refl.symm
Closed-open interval in order dual corresponds to open-closed interval under duality
Informal description
For any elements $a, b$ in a locally finite order $\alpha$, the closed-open interval $\text{Ico}(\text{toDual}(a), \text{toDual}(b))$ in the order dual $\alpha^\text{op}$ is equal to the image of the open-closed interval $\text{Ioc}(b, a)$ in $\alpha$ under the order embedding $\text{toDual}$.
Finset.Ioc_toDual theorem
: Ioc (toDual a) (toDual b) = (Ico b a).map toDual.toEmbedding
Full source 
lemma Finset.Ioc_toDual : Ioc (toDual a) (toDual b) = (Ico b a).map toDual.toEmbedding :=
  map_refl.symm
Open-closed interval in order dual corresponds to closed-open interval under duality
Informal description
For any elements $a, b$ in a locally finite order $\alpha$, the open-closed interval $\text{Ioc}(\text{toDual}(a), \text{toDual}(b))$ in the order dual $\alpha^\text{op}$ is equal to the image of the closed-open interval $\text{Ico}(b, a)$ in $\alpha$ under the order embedding $\text{toDual}$.
Finset.Ioo_toDual theorem
: Ioo (toDual a) (toDual b) = (Ioo b a).map toDual.toEmbedding
Full source 
lemma Finset.Ioo_toDual : Ioo (toDual a) (toDual b) = (Ioo b a).map toDual.toEmbedding :=
  map_refl.symm
Open Interval Correspondence under Order Duality
Informal description
For any elements $a, b$ in a locally finite order $\alpha$, the open interval $\text{Ioo}(\text{toDual}(a), \text{toDual}(b))$ in the order dual $\alpha^\text{op}$ is equal to the image of the open interval $\text{Ioo}(b, a)$ in $\alpha$ under the order embedding $\text{toDual}$.
Finset.Icc_ofDual theorem
(a b : αᵒᵈ) : Icc (ofDual a) (ofDual b) = (Icc b a).map ofDual.toEmbedding
Full source 
lemma Finset.Icc_ofDual (a b : αᵒᵈ) :
    Icc (ofDual a) (ofDual b) = (Icc b a).map ofDual.toEmbedding := map_refl.symm
Closed Interval Correspondence under Order Duality
Informal description
For any elements $a, b$ in the order dual $\alpha^\text{op}$ of a locally finite order $\alpha$, the closed interval $\text{Icc}(\text{ofDual}(a), \text{ofDual}(b))$ in $\alpha$ is equal to the image of the closed interval $\text{Icc}(b, a)$ in $\alpha^\text{op}$ under the order embedding $\text{ofDual}$.
Finset.Ico_ofDual theorem
(a b : αᵒᵈ) : Ico (ofDual a) (ofDual b) = (Ioc b a).map ofDual.toEmbedding
Full source 
lemma Finset.Ico_ofDual (a b : αᵒᵈ) :
    Ico (ofDual a) (ofDual b) = (Ioc b a).map ofDual.toEmbedding := map_refl.symm
Closed-Open Interval Correspondence under Order Duality
Informal description
For any elements $a, b$ in the order dual $\alpha^\text{op}$ of a locally finite order $\alpha$, the closed-open interval $\text{Ico}(\text{ofDual}(a), \text{ofDual}(b))$ in $\alpha$ is equal to the image of the open-closed interval $\text{Ioc}(b, a)$ in $\alpha^\text{op}$ under the order embedding $\text{ofDual}$.
Finset.Ioc_ofDual theorem
(a b : αᵒᵈ) : Ioc (ofDual a) (ofDual b) = (Ico b a).map ofDual.toEmbedding
Full source 
lemma Finset.Ioc_ofDual (a b : αᵒᵈ) :
    Ioc (ofDual a) (ofDual b) = (Ico b a).map ofDual.toEmbedding := map_refl.symm
Open-Closed Interval Correspondence under Order Duality
Informal description
For any elements $a, b$ in the order dual $\alpha^\text{op}$ of a locally finite order $\alpha$, the open-closed interval $\text{Ioc}(\text{ofDual}(a), \text{ofDual}(b))$ in $\alpha$ is equal to the image of the closed-open interval $\text{Ico}(b, a)$ in $\alpha^\text{op}$ under the order embedding $\text{ofDual}$.
Finset.Ioo_ofDual theorem
(a b : αᵒᵈ) : Ioo (ofDual a) (ofDual b) = (Ioo b a).map ofDual.toEmbedding
Full source 
lemma Finset.Ioo_ofDual (a b : αᵒᵈ) :
    Ioo (ofDual a) (ofDual b) = (Ioo b a).map ofDual.toEmbedding := map_refl.symm
Open Interval in Order Dual Corresponds to Reversed Open Interval in Original Order
Informal description
For any elements $a, b$ in the order dual $\alpha^\text{op}$ of a locally finite order $\alpha$, the open interval $\text{Ioo}(a^\text{op}, b^\text{op})$ in $\alpha$ is equal to the image of the open interval $\text{Ioo}(b, a)$ in $\alpha^\text{op}$ under the order embedding that maps elements back to $\alpha$.
OrderDual.instLocallyFiniteOrderBot instance
: LocallyFiniteOrderBot αᵒᵈ
Full source 
/-- Note we define `Iic (toDual a)` as `Ici a` (which has type `Finset α` not `Finset αᵒᵈ`!)
instead of `(Ici a).map toDual.toEmbedding` as this means the following is defeq:
```
lemma this : (Iic (toDual (toDual a)) :) = (Iic a :) := rfl
```
-/
instance OrderDual.instLocallyFiniteOrderBot : LocallyFiniteOrderBot αᵒᵈ where
  finsetIic a := @Ici α _ _ (ofDual a)
  finsetIio a := @Ioi α _ _ (ofDual a)
  finset_mem_Iic _ _ := mem_Ici (α := α)
  finset_mem_Iio _ _ := mem_Ioi (α := α)
Locally Finite Order Structure on Order Duals with Finite Lower-Bounded Intervals
Informal description
The order dual $\alpha^\text{op}$ of a locally finite order $\alpha$ with finite lower-bounded intervals is itself a locally finite order with finite lower-bounded intervals. Specifically, for any element $a$ in $\alpha^\text{op}$, the interval $\text{Iic}(a)$ (elements less than or equal to $a$) is finite and corresponds to the interval $\text{Ici}(a^\text{op})$ (elements greater than or equal to $a^\text{op}$) in $\alpha$.
Iic_orderDual_def theorem
(a : αᵒᵈ) : Iic a = (Ici (ofDual a)).map toDual.toEmbedding
Full source 
lemma Iic_orderDual_def (a : αᵒᵈ) : Iic a = (Ici (ofDual a)).map toDual.toEmbedding := map_refl.symm
Duality of Lower-Closed and Upper-Closed Intervals in Order Duals
Informal description
For any element $a$ in the order dual $\alpha^\text{op}$ of a locally finite order $\alpha$, the lower-closed interval $\text{Iic}(a)$ in $\alpha^\text{op}$ is equal to the image of the upper-closed interval $\text{Ici}(a^\text{op})$ in $\alpha$ under the order embedding that maps each element to its dual.
Iio_orderDual_def theorem
(a : αᵒᵈ) : Iio a = (Ioi (ofDual a)).map toDual.toEmbedding
Full source 
lemma Iio_orderDual_def (a : αᵒᵈ) : Iio a = (Ioi (ofDual a)).map toDual.toEmbedding := map_refl.symm
Duality of Open Lower and Open Upper Intervals in Order Duals
Informal description
For any element $a$ in the order dual $\alpha^\text{op}$ of a locally finite order $\alpha$, the open lower interval $\text{Iio}(a)$ in $\alpha^\text{op}$ is equal to the image of the open upper interval $\text{Ioi}(a^\text{op})$ in $\alpha$ under the order embedding that maps each element to its dual. In other words, $\text{Iio}(a) = \text{Ioi}(a^\text{op})^\text{op}$.
Finset.Iic_toDual theorem
(a : α) : Iic (toDual a) = (Ici a).map toDual.toEmbedding
Full source 
lemma Finset.Iic_toDual (a : α) : Iic (toDual a) = (Ici a).map toDual.toEmbedding :=
  map_refl.symm
Duality of Lower-Closed and Upper-Closed Intervals in Order Duals
Informal description
For any element $a$ in a locally finite order $\alpha$, the finset $\text{Iic}(a^\text{op})$ in the order dual $\alpha^\text{op}$ is equal to the image of the finset $\text{Ici}(a)$ under the order embedding that maps each element to its dual. In other words, the lower-closed interval of the dual of $a$ corresponds to the upper-closed interval of $a$ mapped to the dual order.
Finset.Iio_toDual theorem
(a : α) : Iio (toDual a) = (Ioi a).map toDual.toEmbedding
Full source 
lemma Finset.Iio_toDual (a : α) : Iio (toDual a) = (Ioi a).map toDual.toEmbedding :=
  map_refl.symm
Duality of Open Lower and Open Upper Intervals in Order Duals
Informal description
For any element $a$ in a locally finite order $\alpha$, the finset $\text{Iio}(a^\text{op})$ in the order dual $\alpha^\text{op}$ is equal to the image of the finset $\text{Ioi}(a)$ under the order embedding that maps each element to its dual. In other words, the open lower interval of the dual of $a$ corresponds to the open upper interval of $a$ mapped to the dual order.
Finset.Ici_ofDual theorem
(a : αᵒᵈ) : Ici (ofDual a) = (Iic a).map ofDual.toEmbedding
Full source 
lemma Finset.Ici_ofDual (a : αᵒᵈ) : Ici (ofDual a) = (Iic a).map ofDual.toEmbedding :=
  map_refl.symm
Duality of Upper-Closed and Lower-Closed Intervals via Order Dual
Informal description
For any element $a$ in the order dual $\alpha^\text{op}$ of a locally finite order $\alpha$, the finset $\text{Ici}(a^\text{op})$ (elements greater than or equal to $a^\text{op}$ in $\alpha$) is equal to the image of the finset $\text{Iic}(a)$ (elements less than or equal to $a$ in $\alpha^\text{op}$) under the order embedding that maps each element back to its original form in $\alpha$.
Finset.Ioi_ofDual theorem
(a : αᵒᵈ) : Ioi (ofDual a) = (Iio a).map ofDual.toEmbedding
Full source 
lemma Finset.Ioi_ofDual (a : αᵒᵈ) : Ioi (ofDual a) = (Iio a).map ofDual.toEmbedding :=
  map_refl.symm
Duality of Open Upper and Open Lower Intervals via Order Dual
Informal description
For any element $a$ in the order dual $\alpha^\text{op}$ of a locally finite order $\alpha$, the finset $\text{Ioi}(a^\text{op})$ (elements strictly greater than $a^\text{op}$ in $\alpha$) is equal to the image of the finset $\text{Iio}(a)$ (elements strictly less than $a$ in $\alpha^\text{op}$) under the order embedding that maps each element back to its original form in $\alpha$.
OrderDual.instLocallyFiniteOrderTop instance
: LocallyFiniteOrderTop αᵒᵈ
Full source 
/-- Note we define `Ici (toDual a)` as `Iic a` (which has type `Finset α` not `Finset αᵒᵈ`!)
instead of `(Iic a).map toDual.toEmbedding` as this means the following is defeq:
```
lemma this : (Ici (toDual (toDual a)) :) = (Ici a :) := rfl
```
-/
instance OrderDual.instLocallyFiniteOrderTop : LocallyFiniteOrderTop αᵒᵈ where
  finsetIci a := @Iic α _ _ (ofDual a)
  finsetIoi a := @Iio α _ _ (ofDual a)
  finset_mem_Ici _ _ := mem_Iic (α := α)
  finset_mem_Ioi _ _ := mem_Iio (α := α)
Locally Finite Order Structure on Order Duals
Informal description
The order dual $\alpha^\mathrm{op}$ of a locally finite order $\alpha$ with finite upper-bounded intervals is itself a locally finite order with finite lower-bounded intervals. Specifically, for any element $a$ in $\alpha^\mathrm{op}$, the interval $\text{Ici}(a)$ (elements $\geq a$) corresponds to the interval $\text{Iic}(a^\mathrm{op})$ (elements $\leq a^\mathrm{op}$) in $\alpha$, where $a^\mathrm{op}$ is the dual of $a$ in $\alpha$.
Ici_orderDual_def theorem
(a : αᵒᵈ) : Ici a = (Iic (ofDual a)).map toDual.toEmbedding
Full source 
lemma Ici_orderDual_def (a : αᵒᵈ) : Ici a = (Iic (ofDual a)).map toDual.toEmbedding := map_refl.symm
Duality Correspondence for Closed Upper Intervals: $\text{Ici}(a) = \text{toDual}(\text{Iic}(\text{ofDual}(a)))$
Informal description
For any element $a$ in the order dual $\alpha^\mathrm{op}$ of a locally finite order $\alpha$, the closed upper interval $\text{Ici}(a)$ in $\alpha^\mathrm{op}$ is equal to the image of the closed lower interval $\text{Iic}(\text{ofDual}(a))$ in $\alpha$ under the order embedding $\text{toDual} : \alpha \to \alpha^\mathrm{op}$.
Ioi_orderDual_def theorem
(a : αᵒᵈ) : Ioi a = (Iio (ofDual a)).map toDual.toEmbedding
Full source 
lemma Ioi_orderDual_def (a : αᵒᵈ) : Ioi a = (Iio (ofDual a)).map toDual.toEmbedding := map_refl.symm
Duality Correspondence for Open Upper Intervals: $\text{Ioi}(a) = \text{toDual}(\text{Iio}(\text{ofDual}(a)))$
Informal description
For any element $a$ in the order dual $\alpha^\mathrm{op}$ of a locally finite order $\alpha$, the open upper interval $\text{Ioi}(a)$ in $\alpha^\mathrm{op}$ is equal to the image of the open lower interval $\text{Iio}(\text{ofDual}(a))$ in $\alpha$ under the order embedding $\text{toDual} : \alpha \to \alpha^\mathrm{op}$.
Finset.Ici_toDual theorem
(a : α) : Ici (toDual a) = (Iic a).map toDual.toEmbedding
Full source 
lemma Finset.Ici_toDual (a : α) : Ici (toDual a) = (Iic a).map toDual.toEmbedding :=
  map_refl.symm
Duality Correspondence for Upper-Closed Intervals via Order Dual
Informal description
For any element $a$ in a locally finite order $\alpha$ with finite lower-bounded intervals, the finset $\text{Ici}(\text{toDual}(a))$ (elements $\geq \text{toDual}(a)$ in the order dual $\alpha^\mathrm{op}$) is equal to the image of the finset $\text{Iic}(a)$ (elements $\leq a$ in $\alpha$) under the order embedding $\text{toDual} : \alpha \to \alpha^\mathrm{op}$.
Finset.Ioi_toDual theorem
(a : α) : Ioi (toDual a) = (Iio a).map toDual.toEmbedding
Full source 
lemma Finset.Ioi_toDual (a : α) : Ioi (toDual a) = (Iio a).map toDual.toEmbedding :=
  map_refl.symm
Duality Correspondence for Open Upper Intervals: $\text{Ioi}(\text{toDual}(a)) = \text{toDual}(\text{Iio}(a))$
Informal description
For any element $a$ in a locally finite order $\alpha$, the open upper interval $\text{Ioi}(\text{toDual}(a))$ in the order dual $\alpha^\mathrm{op}$ is equal to the image of the open lower interval $\text{Iio}(a)$ in $\alpha$ under the order embedding $\text{toDual} : \alpha \to \alpha^\mathrm{op}$. In other words, the set of elements strictly greater than the dual of $a$ in $\alpha^\mathrm{op}$ corresponds to the set of elements strictly less than $a$ in $\alpha$, mapped via the duality transformation.
Finset.Iic_ofDual theorem
(a : αᵒᵈ) : Iic (ofDual a) = (Ici a).map ofDual.toEmbedding
Full source 
lemma Finset.Iic_ofDual (a : αᵒᵈ) : Iic (ofDual a) = (Ici a).map ofDual.toEmbedding :=
  map_refl.symm
Duality Correspondence for Lower-Closed Intervals via Order Dual
Informal description
For any element $a$ in the order dual $\alpha^\mathrm{op}$ of a locally finite order $\alpha$ with finite lower-bounded intervals, the finset $\text{Iic}(\text{ofDual}(a))$ (elements $\leq \text{ofDual}(a)$ in $\alpha$) is equal to the image of the finset $\text{Ici}(a)$ (elements $\geq a$ in $\alpha^\mathrm{op}$) under the order embedding $\text{ofDual} : \alpha^\mathrm{op} \to \alpha$.
Finset.Iio_ofDual theorem
(a : αᵒᵈ) : Iio (ofDual a) = (Ioi a).map ofDual.toEmbedding
Full source 
lemma Finset.Iio_ofDual (a : αᵒᵈ) : Iio (ofDual a) = (Ioi a).map ofDual.toEmbedding :=
  map_refl.symm
Duality Correspondence for Open Lower Intervals: $\text{Iio}(\text{ofDual}(a)) = \text{ofDual}(\text{Ioi}(a))$
Informal description
For any element $a$ in the order dual $\alpha^\mathrm{op}$ of a locally finite order $\alpha$, the open lower interval $\text{Iio}(\text{ofDual}(a))$ in $\alpha$ is equal to the image of the open upper interval $\text{Ioi}(a)$ in $\alpha^\mathrm{op}$ under the order embedding $\text{ofDual} : \alpha^\mathrm{op} \to \alpha$. In other words, the set of elements strictly less than the dual element $\text{ofDual}(a)$ in $\alpha$ corresponds to the set of elements strictly greater than $a$ in $\alpha^\mathrm{op}$, mapped via the duality transformation.
Prod.instLocallyFiniteOrder instance
: LocallyFiniteOrder (α × β)
Full source 
instance Prod.instLocallyFiniteOrder : LocallyFiniteOrder (α × β) :=
  LocallyFiniteOrder.ofIcc' (α × β) (fun x y ↦ Icc x.1 y.1 ×ˢ Icc x.2 y.2) fun a b x => by
    rw [mem_product, mem_Icc, mem_Icc, and_and_and_comm, le_def, le_def]
Locally Finite Order Structure on Product of Locally Finite Orders
Informal description
For any two types $\alpha$ and $\beta$ equipped with locally finite order structures, their Cartesian product $\alpha \times \beta$ is also a locally finite order. The finite intervals in the product order are given by the Cartesian product of the corresponding intervals in $\alpha$ and $\beta$. Specifically, for any $(a_1, b_1), (a_2, b_2) \in \alpha \times \beta$, the closed interval $[(a_1, b_1), (a_2, b_2)]$ is equal to $[a_1, a_2] \times [b_1, b_2]$, where $[a_1, a_2]$ and $[b_1, b_2]$ are the corresponding intervals in $\alpha$ and $\beta$ respectively.
Finset.Icc_prod_def theorem
(x y : α × β) : Icc x y = Icc x.1 y.1 ×ˢ Icc x.2 y.2
Full source 
lemma Finset.Icc_prod_def (x y : α × β) : Icc x y = Icc x.1 y.1 ×ˢ Icc x.2 y.2 := rfl
Closed Interval in Product Order as Product of Intervals
Informal description
For any two elements $x = (a_1, b_1)$ and $y = (a_2, b_2)$ in the product order $\alpha \times \beta$ of two locally finite orders, the closed interval $[x, y]$ is equal to the Cartesian product of the closed intervals $[a_1, a_2]$ in $\alpha$ and $[b_1, b_2]$ in $\beta$. In other words, $$ [x, y] = [a_1, a_2] \times [b_1, b_2]. $$
Finset.Icc_product_Icc theorem
(a₁ a₂ : α) (b₁ b₂ : β) : Icc a₁ a₂ ×ˢ Icc b₁ b₂ = Icc (a₁, b₁) (a₂, b₂)
Full source 
lemma Finset.Icc_product_Icc (a₁ a₂ : α) (b₁ b₂ : β) :
    Icc a₁ a₂ ×ˢ Icc b₁ b₂ = Icc (a₁, b₁) (a₂, b₂) := rfl
Product of Closed Intervals Equals Closed Interval in Product Order
Informal description
For any elements $a_1, a_2$ in a locally finite order $\alpha$ and $b_1, b_2$ in a locally finite order $\beta$, the product of the closed intervals $[a_1, a_2] \times [b_1, b_2]$ is equal to the closed interval $[(a_1, b_1), (a_2, b_2)]$ in the product order $\alpha \times \beta$.
Finset.card_Icc_prod theorem
(x y : α × β) : #(Icc x y) = #(Icc x.1 y.1) * #(Icc x.2 y.2)
Full source 
lemma Finset.card_Icc_prod (x y : α × β) : #(Icc x y) = #(Icc x.1 y.1) * #(Icc x.2 y.2) :=
  card_product ..
Cardinality of Closed Interval in Product Order as Product of Cardinalities
Informal description
For any two elements $x = (a_1, b_1)$ and $y = (a_2, b_2)$ in the product order $\alpha \times \beta$ of two locally finite orders, the cardinality of the closed interval $[x, y]$ is equal to the product of the cardinalities of the closed intervals $[a_1, a_2]$ in $\alpha$ and $[b_1, b_2]$ in $\beta$. That is, $$|[x, y]| = |[a_1, a_2]| \cdot |[b_1, b_2]|.$$
Prod.instLocallyFiniteOrderTop instance
: LocallyFiniteOrderTop (α × β)
Full source 
instance Prod.instLocallyFiniteOrderTop : LocallyFiniteOrderTop (α × β) :=
  LocallyFiniteOrderTop.ofIci' (α × β) (fun x => Ici x.1 ×ˢ Ici x.2) fun a x => by
    rw [mem_product, mem_Ici, mem_Ici, le_def]
Locally Finite Order Structure on Product Types with Finite Intervals Bounded Below
Informal description
For any two types $\alpha$ and $\beta$ equipped with locally finite order structures where all intervals bounded below are finite, the product order on $\alpha \times \beta$ also forms a locally finite order where all intervals bounded below are finite. Specifically, for any $(a,b) \in \alpha \times \beta$, the closed-infinite interval $[(a,b), \infty)$ is finite and can be expressed as the product of the corresponding intervals $[a, \infty) \times [b, \infty)$ in $\alpha$ and $\beta$ respectively.
Finset.Ici_prod_def theorem
(x : α × β) : Ici x = Ici x.1 ×ˢ Ici x.2
Full source 
lemma Finset.Ici_prod_def (x : α × β) : Ici x = Ici x.1 ×ˢ Ici x.2 := rfl
Closed-Infinite Interval in Product Order as Cartesian Product
Informal description
For any element $x = (a, b)$ in the product order $\alpha \times \beta$ of two locally finite orders with finite intervals bounded below, the closed-infinite interval $[x, \infty)$ is equal to the Cartesian product of the closed-infinite intervals $[a, \infty)$ in $\alpha$ and $[b, \infty)$ in $\beta$. That is, $$\text{Ici}(x) = \text{Ici}(a) \times \text{Ici}(b).$$
Finset.Ici_product_Ici theorem
(a : α) (b : β) : Ici a ×ˢ Ici b = Ici (a, b)
Full source 
lemma Finset.Ici_product_Ici (a : α) (b : β) : Ici a ×ˢ Ici b = Ici (a, b) := rfl
Product of Closed-Infinite Intervals Equals Closed-Infinite Interval in Product Order
Informal description
For any elements $a$ in a locally finite order $\alpha$ and $b$ in a locally finite order $\beta$, the Cartesian product of the closed-infinite intervals $[a, \infty) \times [b, \infty)$ is equal to the closed-infinite interval $[(a, b), \infty)$ in the product order $\alpha \times \beta$. That is, $$ \text{Ici}(a) \times \text{Ici}(b) = \text{Ici}((a, b)). $$
Finset.card_Ici_prod theorem
(x : α × β) : #(Ici x) = #(Ici x.1) * #(Ici x.2)
Full source 
lemma Finset.card_Ici_prod (x : α × β) : #(Ici x) = #(Ici x.1) * #(Ici x.2) :=
  card_product _ _
Cardinality of Closed-Infinite Interval in Product Order
Informal description
For any element $x = (a, b)$ in the product order $\alpha \times \beta$ of two locally finite orders with finite intervals bounded below, the cardinality of the closed-infinite interval $[x, \infty)$ is equal to the product of the cardinalities of the intervals $[a, \infty)$ in $\alpha$ and $[b, \infty)$ in $\beta$. That is, $$|\text{Ici}(x)| = |\text{Ici}(a)| \cdot |\text{Ici}(b)|.$$
Prod.instLocallyFiniteOrderBot instance
: LocallyFiniteOrderBot (α × β)
Full source 
instance Prod.instLocallyFiniteOrderBot : LocallyFiniteOrderBot (α × β) :=
  LocallyFiniteOrderBot.ofIic' (α × β) (fun x ↦ Iic x.1 ×ˢ Iic x.2) fun a x ↦ by
    rw [mem_product, mem_Iic, mem_Iic, le_def]
Locally Finite Product Order with Finite Lower-Bounded Intervals
Informal description
For any two types $\alpha$ and $\beta$ each equipped with a locally finite order structure where all lower-bounded intervals are finite, the product order on $\alpha \times \beta$ also forms a locally finite order where all lower-bounded intervals are finite. Specifically, for any $(a,b) \in \alpha \times \beta$, the lower-closed interval $\text{Iic}(a,b) = \{(x,y) \mid x \leq a \text{ and } y \leq b\}$ is finite and can be expressed as the product $\text{Iic}(a) \times \text{Iic}(b)$ of finite intervals in $\alpha$ and $\beta$ respectively.
Finset.Iic_prod_def theorem
(x : α × β) : Iic x = Iic x.1 ×ˢ Iic x.2
Full source 
lemma Finset.Iic_prod_def (x : α × β) : Iic x = Iic x.1 ×ˢ Iic x.2 := rfl
Lower-closed interval in product order as Cartesian product of intervals: $\text{Iic}(a,b) = \text{Iic}(a) \times \text{Iic}(b)$
Informal description
For any element $x = (a, b)$ in the product order $\alpha \times \beta$ of two locally finite orders with finite lower-bounded intervals, the lower-closed interval $\text{Iic}(x)$ is equal to the Cartesian product of the lower-closed intervals $\text{Iic}(a) \times \text{Iic}(b)$. In other words, the set of all elements less than or equal to $(a, b)$ in the product order is precisely the product of the sets of elements less than or equal to $a$ in $\alpha$ and less than or equal to $b$ in $\beta$.
Finset.Iic_product_Iic theorem
(a : α) (b : β) : Iic a ×ˢ Iic b = Iic (a, b)
Full source 
lemma Finset.Iic_product_Iic (a : α) (b : β) : Iic a ×ˢ Iic b = Iic (a, b) := rfl
Product of Lower-Closed Intervals Equals Lower-Closed Interval in Product Order
Informal description
For any elements $a$ in a locally finite order $\alpha$ and $b$ in a locally finite order $\beta$, the Cartesian product of the lower-closed intervals $\text{Iic}(a) \times \text{Iic}(b)$ is equal to the lower-closed interval $\text{Iic}(a, b)$ in the product order $\alpha \times \beta$.
Finset.card_Iic_prod theorem
(x : α × β) : #(Iic x) = #(Iic x.1) * #(Iic x.2)
Full source 
lemma Finset.card_Iic_prod (x : α × β) : #(Iic x) = #(Iic x.1) * #(Iic x.2) := card_product ..
Cardinality of Lower-Closed Interval in Product Order: $|\text{Iic}(x_1, x_2)| = |\text{Iic}(x_1)| \cdot |\text{Iic}(x_2)|$
Informal description
For any element $x = (x_1, x_2)$ in the product order $\alpha \times \beta$ of two locally finite orders with finite lower-bounded intervals, the cardinality of the lower-closed interval $\text{Iic}(x)$ is equal to the product of the cardinalities of the lower-closed intervals $\text{Iic}(x_1)$ in $\alpha$ and $\text{Iic}(x_2)$ in $\beta$. That is, $|\text{Iic}(x)| = |\text{Iic}(x_1)| \cdot |\text{Iic}(x_2)|$.
Finset.uIcc_prod_def theorem
(x y : α × β) : uIcc x y = uIcc x.1 y.1 ×ˢ uIcc x.2 y.2
Full source 
lemma Finset.uIcc_prod_def (x y : α × β) : uIcc x y = uIcc x.1 y.1 ×ˢ uIcc x.2 y.2 := rfl
Unordered Interval in Product Order as Cartesian Product of Intervals
Informal description
For any elements $x = (x_1, x_2)$ and $y = (y_1, y_2)$ in the product order $\alpha \times \beta$ of two locally finite orders, the unordered closed interval $\text{uIcc}(x, y)$ is equal to the Cartesian product of the unordered closed intervals $\text{uIcc}(x_1, y_1) \times \text{uIcc}(x_2, y_2)$.
Finset.uIcc_product_uIcc theorem
(a₁ a₂ : α) (b₁ b₂ : β) : uIcc a₁ a₂ ×ˢ uIcc b₁ b₂ = uIcc (a₁, b₁) (a₂, b₂)
Full source 
lemma Finset.uIcc_product_uIcc (a₁ a₂ : α) (b₁ b₂ : β) :
    uIcc a₁ a₂ ×ˢ uIcc b₁ b₂ = uIcc (a₁, b₁) (a₂, b₂) := rfl
Product of Unordered Intervals Equals Unordered Interval in Product Order
Informal description
For any elements $a_1, a_2$ in a locally finite order $\alpha$ and $b_1, b_2$ in a locally finite order $\beta$, the product of the unordered closed intervals $\text{uIcc}(a_1, a_2) \times \text{uIcc}(b_1, b_2)$ is equal to the unordered closed interval $\text{uIcc}((a_1, b_1), (a_2, b_2))$ in the product order $\alpha \times \beta$.
Finset.card_uIcc_prod theorem
(x y : α × β) : #(uIcc x y) = #(uIcc x.1 y.1) * #(uIcc x.2 y.2)
Full source 
lemma Finset.card_uIcc_prod (x y : α × β) : #(uIcc x y) = #(uIcc x.1 y.1) * #(uIcc x.2 y.2) :=
  card_product ..
Cardinality of Unordered Interval in Product Order as Product of Cardinalities
Informal description
For any elements $x = (x_1, x_2)$ and $y = (y_1, y_2)$ in the product order $\alpha \times \beta$ of two locally finite orders, the cardinality of the unordered closed interval $\text{uIcc}(x, y)$ is equal to the product of the cardinalities of the unordered closed intervals $\text{uIcc}(x_1, y_1)$ in $\alpha$ and $\text{uIcc}(x_2, y_2)$ in $\beta$. That is, $$|\text{uIcc}(x, y)| = |\text{uIcc}(x_1, y_1)| \cdot |\text{uIcc}(x_2, y_2)|.$$
WithTop.insertTop definition
: Finset α ↪o Finset (WithTop α)
Full source 
/-- Given a finset on `α`, lift it to being a finset on `WithTop α`
using `WithTop.some` and then insert `⊤`. -/
def insertTop : FinsetFinset α ↪o Finset (WithTop α) :=
  OrderEmbedding.ofMapLEIff
    (fun s => cons ⊤ (s.map Embedding.coeWithTop) <| by simp)
    (fun s t => by rw [le_iff_subset, cons_subset_cons, map_subset_map, le_iff_subset])
Lifting finset to WithTop with top element added
Informal description
Given a finset $s$ on a type $\alpha$, the function `WithTop.insertTop` lifts $s$ to a finset on $\text{WithTop}\ \alpha$ by first mapping each element of $s$ to $\text{WithTop}\ \alpha$ via the canonical embedding $\text{WithTop.some}$ and then inserting the top element $\top$. This defines an order embedding from the finsets on $\alpha$ to the finsets on $\text{WithTop}\ \alpha$.
WithTop.some_mem_insertTop theorem
{s : Finset α} {a : α} : ↑a ∈ insertTop s ↔ a ∈ s
Full source 
@[simp]
theorem some_mem_insertTop {s : Finset α} {a : α} : ↑a ∈ insertTop s↑a ∈ insertTop s ↔ a ∈ s := by
  simp [insertTop]
Membership in Lifted Finset via `WithTop.some`
Informal description
For any finset $s$ of elements of type $\alpha$ and any element $a \in \alpha$, the lifted element $\text{some}(a)$ belongs to the finset $\text{insertTop}(s)$ if and only if $a$ belongs to $s$.
WithTop.top_mem_insertTop theorem
{s : Finset α} : ⊤ ∈ insertTop s
Full source 
@[simp]
theorem top_mem_insertTop {s : Finset α} : ⊤⊤ ∈ insertTop s := by
  simp [insertTop]
Top Element Belongs to Inserted Top Finset
Informal description
For any finset $s$ of elements of type $\alpha$, the top element $\top$ is a member of the finset obtained by applying the embedding $\text{insertTop}$ to $s$.
WithTop.locallyFiniteOrder instance
: LocallyFiniteOrder (WithTop α)
Full source 
instance locallyFiniteOrder : LocallyFiniteOrder (WithTop α) where
  finsetIcc a b :=
    match a, b with
    | ⊤, ⊤ => {⊤}
    | ⊤, (b : α) => ∅
    | (a : α), ⊤ => insertTop (Ici a)
    | (a : α), (b : α) => (Icc a b).map Embedding.coeWithTop
  finsetIco a b :=
    match a, b with
    | ⊤, _ => ∅
    | (a : α), ⊤ => (Ici a).map Embedding.coeWithTop
    | (a : α), (b : α) => (Ico a b).map Embedding.coeWithTop
  finsetIoc a b :=
    match a, b with
    | ⊤, _ => ∅
    | (a : α), ⊤ => insertTop (Ioi a)
    | (a : α), (b : α) => (Ioc a b).map Embedding.coeWithTop
  finsetIoo a b :=
    match a, b with
    | ⊤, _ => ∅
    | (a : α), ⊤ => (Ioi a).map Embedding.coeWithTop
    | (a : α), (b : α) => (Ioo a b).map Embedding.coeWithTop
  finset_mem_Icc a b x := by
    cases a <;> cases b <;> cases x <;> simp
  finset_mem_Ico a b x := by
    cases a <;> cases b <;> cases x <;> simp
  finset_mem_Ioc a b x := by
    cases a <;> cases b <;> cases x <;> simp
  finset_mem_Ioo a b x := by
    cases a <;> cases b <;> cases x <;> simp
Locally Finite Order Structure on $\text{WithTop}\ \alpha$
Informal description
For any type $\alpha$ with a locally finite order, the type $\text{WithTop}\ \alpha$ (obtained by adding a top element $\top$ to $\alpha$) also has a canonical locally finite order structure. This means that all bounded intervals in $\text{WithTop}\ \alpha$ are finite, including intervals involving the top element $\top$.
WithTop.Icc_coe_top theorem
: Icc (a : WithTop α) ⊤ = insertNone (Ici a)
Full source 
theorem Icc_coe_top : Icc (a : WithTop α) ⊤ = insertNone (Ici a) :=
  rfl
Closed Interval from Element to Top in WithTop Equals Inserted Closed-Infinite Interval
Informal description
For any element $a$ in a locally finite order $\alpha$, the closed interval $[a, \top]$ in $\text{WithTop}\ \alpha$ is equal to the finset obtained by inserting $\top$ into the image of the closed-infinite interval $[a, \infty)$ under the canonical embedding of $\alpha$ into $\text{WithTop}\ \alpha$.
WithTop.Icc_coe_coe theorem
: Icc (a : WithTop α) b = (Icc a b).map Embedding.some
Full source 
theorem Icc_coe_coe : Icc (a : WithTop α) b = (Icc a b).map Embedding.some :=
  rfl
Closed Interval Embedding in $\text{WithTop}\ \alpha$: $[a, b] = \text{some}([a, b])$
Informal description
For any elements $a, b$ in a locally finite order $\alpha$, the closed interval $[a, b]$ in $\text{WithTop}\ \alpha$ (where $a$ and $b$ are considered as elements of $\text{WithTop}\ \alpha$ via the embedding $\text{some}$) is equal to the image of the closed interval $[a, b]$ in $\alpha$ under the embedding $\text{some}$.
WithTop.Ico_coe_top theorem
: Ico (a : WithTop α) ⊤ = (Ici a).map Embedding.some
Full source 
theorem Ico_coe_top : Ico (a : WithTop α) ⊤ = (Ici a).map Embedding.some :=
  rfl
Closed-Open Interval at Top in $\text{WithTop}\ \alpha$ as Image of Closed Infinite Interval
Informal description
For any element $a$ in a locally finite order $\alpha$ extended with a top element $\top$, the closed-open interval $[a, \top)$ in $\text{WithTop}\ \alpha$ is equal to the image of the closed infinite interval $[a, \infty)$ in $\alpha$ under the embedding $\text{Embedding.some}$ (which maps elements of $\alpha$ to $\text{WithTop}\ \alpha$). In other words, $\text{Ico}(a, \top) = \text{Embedding.some}(\text{Ici}(a))$.
WithTop.Ico_coe_coe theorem
: Ico (a : WithTop α) b = (Ico a b).map Embedding.some
Full source 
theorem Ico_coe_coe : Ico (a : WithTop α) b = (Ico a b).map Embedding.some :=
  rfl
Closed-Open Interval in $\text{WithTop}\ \alpha$ as Image of Interval in $\alpha$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the closed-open interval $[a, b)$ in $\text{WithTop}\ \alpha$ (where $a$ and $b$ are considered as elements of $\text{WithTop}\ \alpha$ via the embedding $\text{some}$) is equal to the image of the closed-open interval $[a, b)$ in $\alpha$ under the embedding $\text{some}$. In other words, $\text{Ico}(a, b) = \text{some}(\text{Ico}(a, b))$ as finsets.
WithTop.Ioc_coe_top theorem
: Ioc (a : WithTop α) ⊤ = insertNone (Ioi a)
Full source 
theorem Ioc_coe_top : Ioc (a : WithTop α) ⊤ = insertNone (Ioi a) :=
  rfl
Open-Closed Interval at Top in $\text{WithTop}\ \alpha$ as Image of Open Infinite Interval
Informal description
For any element $a$ in a locally finite order $\alpha$ extended with a top element $\top$, the open-closed interval $(a, \top]$ in $\text{WithTop}\ \alpha$ is equal to the image of the open infinite interval $(a, \infty)$ in $\alpha$ under the embedding $\text{insertNone}$ (which maps elements of $\alpha$ to $\text{WithTop}\ \alpha$). In other words, $\text{Ioc}(a, \top) = \text{insertNone}(\text{Ioi}(a))$.
WithTop.Ioc_coe_coe theorem
: Ioc (a : WithTop α) b = (Ioc a b).map Embedding.some
Full source 
theorem Ioc_coe_coe : Ioc (a : WithTop α) b = (Ioc a b).map Embedding.some :=
  rfl
Open-Closed Interval in $\text{WithTop}\ \alpha$ as Image of Interval in $\alpha$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the open-closed interval $(a, b]$ in $\text{WithTop}\ \alpha$ (where $a$ and $b$ are considered as elements of $\text{WithTop}\ \alpha$ via the embedding $\text{some}$) is equal to the image of the open-closed interval $(a, b]$ in $\alpha$ under the embedding $\text{some}$. In other words, $\text{Ioc}(a, b) = \text{some}(\text{Ioc}(a, b))$ as finsets.
WithTop.Ioo_coe_top theorem
: Ioo (a : WithTop α) ⊤ = (Ioi a).map Embedding.some
Full source 
theorem Ioo_coe_top : Ioo (a : WithTop α) ⊤ = (Ioi a).map Embedding.some :=
  rfl
Open Interval at Top in $\text{WithTop}\ \alpha$ as Image of Open Infinite Interval
Informal description
For any element $a$ in a locally finite order $\alpha$, the open interval $(a, \top)$ in $\text{WithTop}\ \alpha$ is equal to the image of the open infinite interval $(a, \infty)$ in $\alpha$ under the embedding $\text{some}$. In other words, $\text{Ioo}(a, \top) = \text{some}(\text{Ioi}(a))$ as finsets.
WithTop.Ioo_coe_coe theorem
: Ioo (a : WithTop α) b = (Ioo a b).map Embedding.some
Full source 
theorem Ioo_coe_coe : Ioo (a : WithTop α) b = (Ioo a b).map Embedding.some :=
  rfl
Open Interval in $\text{WithTop}\ \alpha$ as Image of Open Interval in $\alpha$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the open interval $(a, b)$ in $\text{WithTop}\ \alpha$ (where $a$ and $b$ are considered as elements of $\text{WithTop}\ \alpha$ via the embedding $\text{some}$) is equal to the image of the open interval $(a, b)$ in $\alpha$ under the embedding $\text{some}$. In other words, $\text{Ioo}(a, b) = \text{some}(\text{Ioo}(a, b))$ as finsets.
WithBot.insertBot definition
: Finset α ↪o Finset (WithBot α)
Full source 
/-- Given a finset on `α`, lift it to being a finset on `WithBot α`
using `WithBot.some` and then insert `⊥`. -/
def insertBot : FinsetFinset α ↪o Finset (WithBot α) :=
  OrderEmbedding.ofMapLEIff
    (fun s => cons ⊥ (s.map Embedding.coeWithBot) <| by simp)
    (fun s t => by rw [le_iff_subset, cons_subset_cons, map_subset_map, le_iff_subset])
Lifting finset to `WithBot` with bottom element inclusion
Informal description
Given a finset $s$ on a type $\alpha$, the function `WithBot.insertBot` lifts $s$ to a finset on `WithBot α` by first mapping each element of $s$ to `WithBot α` via the embedding `WithBot.some` and then inserting the bottom element $\bot$. This results in an order embedding from the finsets on $\alpha$ to the finsets on `WithBot α`.
WithBot.some_mem_insertBot theorem
{s : Finset α} {a : α} : ↑a ∈ insertBot s ↔ a ∈ s
Full source 
@[simp]
theorem some_mem_insertBot {s : Finset α} {a : α} : ↑a ∈ insertBot s↑a ∈ insertBot s ↔ a ∈ s := by
  simp [insertBot]
Membership in `insertBot` finset corresponds to membership in original finset
Informal description
For any finset $s$ of elements of type $\alpha$ and any element $a \in \alpha$, the element $a$ lifted to `WithBot α` (denoted as $\uparrow a$) is a member of the finset obtained by applying the `insertBot` function to $s$ if and only if $a$ is a member of $s$.
WithBot.bot_mem_insertBot theorem
{s : Finset α} : ⊥ ∈ insertBot s
Full source 
@[simp]
theorem bot_mem_insertBot {s : Finset α} : ⊥⊥ ∈ insertBot s := by
  simp [insertBot]
Bottom Element Belongs to `insertBot` Finset
Informal description
For any finset $s$ of elements of type $\alpha$, the bottom element $\bot$ is a member of the finset obtained by applying the `insertBot` function to $s$.
WithBot.instLocallyFiniteOrder instance
: LocallyFiniteOrder (WithBot α)
Full source 
instance instLocallyFiniteOrder : LocallyFiniteOrder (WithBot α) :=
  OrderDual.instLocallyFiniteOrder (α := WithTop αᵒᵈ)
The Locally Finite Order Structure on $\text{WithBot}\ \alpha$
Informal description
For any type $\alpha$ with a locally finite order, the type $\text{WithBot}\ \alpha$ (obtained by adding a bottom element $\bot$ to $\alpha$) also has a canonical locally finite order structure. This means that all bounded intervals in $\text{WithBot}\ \alpha$ are finite, including intervals involving the bottom element $\bot$.
WithBot.Icc_bot_coe theorem
: Icc (⊥ : WithBot α) b = insertNone (Iic b)
Full source 
theorem Icc_bot_coe : Icc (⊥ : WithBot α) b = insertNone (Iic b) :=
  rfl
Closed Interval from Bottom to $b$ in $\text{WithBot}\ \alpha$ Equals Inserted Lower-Closed Interval
Informal description
For any element $b$ in a locally finite order $\alpha$ with a bottom element $\bot$, the closed interval $[\bot, b]$ in $\text{WithBot}\ \alpha$ is equal to the finset obtained by inserting $\bot$ into the lower-closed interval $(-\infty, b]$ of $\alpha$.
WithBot.Icc_coe_coe theorem
: Icc (a : WithBot α) b = (Icc a b).map Embedding.some
Full source 
theorem Icc_coe_coe : Icc (a : WithBot α) b = (Icc a b).map Embedding.some :=
  rfl
Closed Interval in $\text{WithBot}\ \alpha$ via Embedding
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the closed interval $[a, b]$ in $\text{WithBot}\ \alpha$ (where $a$ and $b$ are considered as elements of $\text{WithBot}\ \alpha$ via the natural embedding) is equal to the image of the closed interval $[a, b]$ in $\alpha$ under the embedding map.
WithBot.Ico_bot_coe theorem
: Ico (⊥ : WithBot α) b = insertNone (Iio b)
Full source 
theorem Ico_bot_coe : Ico (⊥ : WithBot α) b = insertNone (Iio b) :=
  rfl
Half-Open Interval from Bottom to $b$ in $\text{WithBot}\ \alpha$ Equals Inserted Open Lower Interval
Informal description
For any element $b$ in a locally finite order $\alpha$ with a bottom element $\bot$, the half-open interval $[\bot, b)$ in $\text{WithBot}\ \alpha$ is equal to the finset obtained by inserting $\bot$ into the open lower interval $(-\infty, b)$ of $\alpha$.
WithBot.Ico_coe_coe theorem
: Ico (a : WithBot α) b = (Ico a b).map Embedding.some
Full source 
theorem Ico_coe_coe : Ico (a : WithBot α) b = (Ico a b).map Embedding.some :=
  rfl
Closed-open interval in $\text{WithBot}\ \alpha$ via embedding
Informal description
For any elements $a, b$ in a locally finite order $\alpha$, the closed-open interval $[a, b)$ in $\text{WithBot}\ \alpha$ (where $a$ and $b$ are lifted from $\alpha$) is equal to the image of the corresponding interval $[a, b)$ in $\alpha$ under the embedding $\text{some} : \alpha \to \text{WithBot}\ \alpha$. In other words, $\text{Ico}(a, b) = \text{some}(\text{Ico}(a, b))$ as finsets in $\text{WithBot}\ \alpha$.
WithBot.Ioc_bot_coe theorem
: Ioc (⊥ : WithBot α) b = (Iic b).map Embedding.some
Full source 
theorem Ioc_bot_coe : Ioc (⊥ : WithBot α) b = (Iic b).map Embedding.some :=
  rfl
Open-Closed Interval from Bottom in WithBot Equals Image of Lower-Closed Interval
Informal description
For a locally finite order $\alpha$ and an element $b \in \alpha$, the open-closed interval $(\bot, b]$ in $\text{WithBot}\ \alpha$ is equal to the image of the lower-closed interval $(-\infty, b]$ in $\alpha$ under the embedding that maps elements of $\alpha$ to their corresponding elements in $\text{WithBot}\ \alpha$.
WithBot.Ioc_coe_coe theorem
: Ioc (a : WithBot α) b = (Ioc a b).map Embedding.some
Full source 
theorem Ioc_coe_coe : Ioc (a : WithBot α) b = (Ioc a b).map Embedding.some :=
  rfl
Open-Closed Interval in $\text{WithBot}\ \alpha$ via Embedding
Informal description
For elements $a, b$ in a locally finite order $\alpha$, the open-closed interval $\text{Ioc}(a, b)$ in $\text{WithBot}\ \alpha$ (where $a$ and $b$ are considered as elements of $\text{WithBot}\ \alpha$ via the embedding $\text{some}$) is equal to the image of the open-closed interval $\text{Ioc}(a, b)$ in $\alpha$ under the embedding $\text{some}$.
WithBot.Ioo_bot_coe theorem
: Ioo (⊥ : WithBot α) b = (Iio b).map Embedding.some
Full source 
theorem Ioo_bot_coe : Ioo (⊥ : WithBot α) b = (Iio b).map Embedding.some :=
  rfl
Open Interval from Bottom to $b$ in $\text{WithBot}\ \alpha$ Equals Embedded Lower Interval
Informal description
For an element $b$ in the type $\text{WithBot}\ \alpha$ (where $\alpha$ is a locally finite order), the open interval $(\bot, b)$ is equal to the image of the open lower interval $(-\infty, b)$ under the embedding of $\alpha$ into $\text{WithBot}\ \alpha$. In other words, the set $\{x \mid \bot < x < b\}$ is the same as the set $\{x \mid x < b\}$ embedded into $\text{WithBot}\ \alpha$.
WithBot.Ioo_coe_coe theorem
: Ioo (a : WithBot α) b = (Ioo a b).map Embedding.some
Full source 
theorem Ioo_coe_coe : Ioo (a : WithBot α) b = (Ioo a b).map Embedding.some :=
  rfl
Open Interval in $\text{WithBot}\ \alpha$ via Embedding
Informal description
For any elements $a, b$ in a locally finite order $\alpha$, the open interval $(a, b)$ in $\text{WithBot}\ \alpha$ (where $a$ and $b$ are considered as elements of $\text{WithBot}\ \alpha$ via the embedding $\text{some}$) is equal to the image of the open interval $(a, b)$ in $\alpha$ under the embedding $\text{some}$.
OrderIso.locallyFiniteOrder abbrev
[LocallyFiniteOrder β] (f : α ≃o β) : LocallyFiniteOrder α
Full source 
/-- Transfer `LocallyFiniteOrder` across an `OrderIso`. -/
abbrev locallyFiniteOrder [LocallyFiniteOrder β] (f : α ≃o β) : LocallyFiniteOrder α where
  finsetIcc a b := (Icc (f a) (f b)).map f.symm.toEquiv.toEmbedding
  finsetIco a b := (Ico (f a) (f b)).map f.symm.toEquiv.toEmbedding
  finsetIoc a b := (Ioc (f a) (f b)).map f.symm.toEquiv.toEmbedding
  finsetIoo a b := (Ioo (f a) (f b)).map f.symm.toEquiv.toEmbedding
  finset_mem_Icc := by simp
  finset_mem_Ico := by simp
  finset_mem_Ioc := by simp
  finset_mem_Ioo := by simp
Transfer of Locally Finite Order via Order Isomorphism
Informal description
Given an order isomorphism $f : \alpha \simeq \beta$ between preorders $\alpha$ and $\beta$, if $\beta$ is a locally finite order, then $\alpha$ is also a locally finite order. This means that for any $a, b \in \alpha$, the intervals $[a, b]$, $[a, b)$, $(a, b]$, and $(a, b)$ in $\alpha$ are finite, since they correspond via $f$ to finite intervals in $\beta$.
OrderIso.locallyFiniteOrderTop abbrev
[LocallyFiniteOrderTop β] (f : α ≃o β) : LocallyFiniteOrderTop α
Full source 
/-- Transfer `LocallyFiniteOrderTop` across an `OrderIso`. -/
abbrev locallyFiniteOrderTop [LocallyFiniteOrderTop β] (f : α ≃o β) : LocallyFiniteOrderTop α where
  finsetIci a := (Ici (f a)).map f.symm.toEquiv.toEmbedding
  finsetIoi a := (Ioi (f a)).map f.symm.toEquiv.toEmbedding
  finset_mem_Ici := by simp
  finset_mem_Ioi := by simp
Transfer of Locally Finite Order Top Structure via Order Isomorphism
Informal description
Given an order isomorphism $f : \alpha \simeq \beta$ between preorders $\alpha$ and $\beta$, if $\beta$ has the structure of a locally finite order with finite intervals bounded below (i.e., $\beta$ is a `LocallyFiniteOrderTop`), then $\alpha$ inherits this structure via $f$.
OrderIso.locallyFiniteOrderBot abbrev
[LocallyFiniteOrderBot β] (f : α ≃o β) : LocallyFiniteOrderBot α
Full source 
/-- Transfer `LocallyFiniteOrderBot` across an `OrderIso`. -/
abbrev locallyFiniteOrderBot [LocallyFiniteOrderBot β] (f : α ≃o β) : LocallyFiniteOrderBot α where
  finsetIic a := (Iic (f a)).map f.symm.toEquiv.toEmbedding
  finsetIio a := (Iio (f a)).map f.symm.toEquiv.toEmbedding
  finset_mem_Iic := by simp
  finset_mem_Iio := by simp
Transfer of Locally Finite Order with Finite Lower-Bounded Intervals via Order Isomorphism
Informal description
Given an order isomorphism $f : \alpha \simeq \beta$ between preorders $\alpha$ and $\beta$, if $\beta$ is a locally finite order with finite lower-bounded intervals, then $\alpha$ inherits this structure via $f$. Specifically, for any $b \in \alpha$, the intervals $\text{Iic}(b)$ and $\text{Iio}(b)$ in $\alpha$ are finite.
Subtype.instLocallyFiniteOrder instance
[LocallyFiniteOrder α] : LocallyFiniteOrder (Subtype p)
Full source 
instance Subtype.instLocallyFiniteOrder [LocallyFiniteOrder α] :
    LocallyFiniteOrder (Subtype p) where
  finsetIcc a b := (Icc (a : α) b).subtype p
  finsetIco a b := (Ico (a : α) b).subtype p
  finsetIoc a b := (Ioc (a : α) b).subtype p
  finsetIoo a b := (Ioo (a : α) b).subtype p
  finset_mem_Icc a b x := by simp_rw [Finset.mem_subtype, mem_Icc, Subtype.coe_le_coe]
  finset_mem_Ico a b x := by
    simp_rw [Finset.mem_subtype, mem_Ico, Subtype.coe_le_coe, Subtype.coe_lt_coe]
  finset_mem_Ioc a b x := by
    simp_rw [Finset.mem_subtype, mem_Ioc, Subtype.coe_le_coe, Subtype.coe_lt_coe]
  finset_mem_Ioo a b x := by simp_rw [Finset.mem_subtype, mem_Ioo, Subtype.coe_lt_coe]
Subtype Inherits Locally Finite Order Structure
Informal description
For any preorder $\alpha$ that is a locally finite order and any predicate $p$ on $\alpha$, the subtype $\{x \in \alpha \mid p(x)\}$ inherits the structure of a locally finite order. This means that for any two elements $a, b$ in the subtype, the intervals $[a, b]$, $[a, b)$, $(a, b]$, and $(a, b)$ are all finite sets.
Subtype.instLocallyFiniteOrderTop instance
[LocallyFiniteOrderTop α] : LocallyFiniteOrderTop (Subtype p)
Full source 
instance Subtype.instLocallyFiniteOrderTop [LocallyFiniteOrderTop α] :
    LocallyFiniteOrderTop (Subtype p) where
  finsetIci a := (Ici (a : α)).subtype p
  finsetIoi a := (Ioi (a : α)).subtype p
  finset_mem_Ici a x := by simp_rw [Finset.mem_subtype, mem_Ici, Subtype.coe_le_coe]
  finset_mem_Ioi a x := by simp_rw [Finset.mem_subtype, mem_Ioi, Subtype.coe_lt_coe]
Subtype Inherits Locally Finite Order with Finite Upper-Bounded Intervals
Informal description
For any preorder $\alpha$ that is a locally finite order with finite upper-bounded intervals, and any predicate $p$ on $\alpha$, the subtype $\{x \in \alpha \mid p(x)\}$ inherits the structure of a locally finite order with finite upper-bounded intervals. This means that for any element $a$ in the subtype, the intervals $\text{Ici}(a)$ and $\text{Ioi}(a)$ are finite sets.
Subtype.instLocallyFiniteOrderBot instance
[LocallyFiniteOrderBot α] : LocallyFiniteOrderBot (Subtype p)
Full source 
instance Subtype.instLocallyFiniteOrderBot [LocallyFiniteOrderBot α] :
    LocallyFiniteOrderBot (Subtype p) where
  finsetIic a := (Iic (a : α)).subtype p
  finsetIio a := (Iio (a : α)).subtype p
  finset_mem_Iic a x := by simp_rw [Finset.mem_subtype, mem_Iic, Subtype.coe_le_coe]
  finset_mem_Iio a x := by simp_rw [Finset.mem_subtype, mem_Iio, Subtype.coe_lt_coe]
Subtype Inherits Locally Finite Order with Finite Lower-Bounded Intervals
Informal description
For any preorder $\alpha$ that is a locally finite order with finite lower-bounded intervals, and any predicate $p$ on $\alpha$, the subtype $\{x \in \alpha \mid p(x)\}$ inherits the structure of a locally finite order with finite lower-bounded intervals. This means that for any element $b$ in the subtype, the intervals $\text{Iic}(b)$ and $\text{Iio}(b)$ are finite sets.
Finset.subtype_Icc_eq theorem
: Icc a b = (Icc (a : α) b).subtype p
Full source 
theorem subtype_Icc_eq : Icc a b = (Icc (a : α) b).subtype p :=
  rfl
Subtype Closed Interval Equality
Informal description
For a locally finite order $\alpha$ and a predicate $p$ on $\alpha$, the closed interval $[a, b]$ in the subtype $\{x \in \alpha \mid p(x)\}$ is equal to the subtype of the closed interval $[a, b]$ in $\alpha$ restricted to elements satisfying $p$. In other words, $\text{Icc}(a, b) = \{x \in \text{Icc}(a, b) \mid p(x)\}$.
Finset.subtype_Ico_eq theorem
: Ico a b = (Ico (a : α) b).subtype p
Full source 
theorem subtype_Ico_eq : Ico a b = (Ico (a : α) b).subtype p :=
  rfl
Subtype Closed-Open Interval Equality
Informal description
For a locally finite order $\alpha$ and a predicate $p$ on $\alpha$, the closed-open interval $[a, b)$ in the subtype $\{x \in \alpha \mid p(x)\}$ is equal to the subtype of the closed-open interval $[a, b)$ in $\alpha$ restricted to elements satisfying $p$. In other words, $\text{Ico}(a, b) = \{x \in \text{Ico}(a, b) \mid p(x)\}$.
Finset.subtype_Ioc_eq theorem
: Ioc a b = (Ioc (a : α) b).subtype p
Full source 
theorem subtype_Ioc_eq : Ioc a b = (Ioc (a : α) b).subtype p :=
  rfl
Subtype Open-Closed Interval Equality
Informal description
For a locally finite order $\alpha$ and a predicate $p$ on $\alpha$, the open-closed interval $(a, b]$ in the subtype $\{x \in \alpha \mid p(x)\}$ is equal to the subtype of the open-closed interval $(a, b]$ in $\alpha$ restricted to elements satisfying $p$. In other words, $\text{Ioc}(a, b) = \{x \in \text{Ioc}(a, b) \mid p(x)\}$.
Finset.subtype_Ioo_eq theorem
: Ioo a b = (Ioo (a : α) b).subtype p
Full source 
theorem subtype_Ioo_eq : Ioo a b = (Ioo (a : α) b).subtype p :=
  rfl
Subtype Open Interval Equality
Informal description
For a locally finite order $\alpha$ and a predicate $p$ on $\alpha$, the open interval $(a, b)$ in the subtype $\{x \in \alpha \mid p(x)\}$ is equal to the subtype of the open interval $(a, b)$ in $\alpha$ restricted to elements satisfying $p$. In other words, $\text{Ioo}(a, b) = \{x \in \text{Ioo}(a, b) \mid p(x)\}$.
Finset.map_subtype_embedding_Icc theorem
(hp : ∀ ⦃a b x⦄, a ≤ x → x ≤ b → p a → p b → p x) : (Icc a b).map (Embedding.subtype p) = (Icc a b : Finset α)
Full source 
theorem map_subtype_embedding_Icc (hp : ∀ ⦃a b x⦄, a ≤ x → x ≤ b → p a → p b → p x):
    (Icc a b).map (Embedding.subtype p) = (Icc a b : Finset α) := by
  rw [subtype_Icc_eq]
  refine Finset.subtype_map_of_mem fun x hx => ?_
  rw [mem_Icc] at hx
  exact hp hx.1 hx.2 a.prop b.prop
Image of Subtype Closed Interval under Embedding Equals Original Closed Interval
Informal description
Let $\alpha$ be a locally finite order and $p$ a predicate on $\alpha$ such that for any $a, b, x \in \alpha$, if $a \leq x \leq b$ and both $p(a)$ and $p(b)$ hold, then $p(x)$ also holds. Then the image of the closed interval $[a, b]$ in the subtype $\{x \in \alpha \mid p(x)\}$ under the canonical embedding is equal to the closed interval $[a, b]$ in $\alpha$ itself, considered as a finset.
Finset.map_subtype_embedding_Ico theorem
(hp : ∀ ⦃a b x⦄, a ≤ x → x ≤ b → p a → p b → p x) : (Ico a b).map (Embedding.subtype p) = (Ico a b : Finset α)
Full source 
theorem map_subtype_embedding_Ico (hp : ∀ ⦃a b x⦄, a ≤ x → x ≤ b → p a → p b → p x):
    (Ico a b).map (Embedding.subtype p) = (Ico a b : Finset α) := by
  rw [subtype_Ico_eq]
  refine Finset.subtype_map_of_mem fun x hx => ?_
  rw [mem_Ico] at hx
  exact hp hx.1 hx.2.le a.prop b.prop
Subtype Embedding Preserves Closed-Open Interval Finset under Convexity Condition
Informal description
Let $\alpha$ be a locally finite order and $p$ a predicate on $\alpha$ such that for any $a, b, x \in \alpha$ with $a \leq x \leq b$, if $p(a)$ and $p(b)$ hold, then $p(x)$ also holds. Then the image of the closed-open interval finset $\text{Ico}(a, b)$ under the subtype embedding map is equal to the closed-open interval finset $\text{Ico}(a, b)$ in $\alpha$.
Finset.map_subtype_embedding_Ioc theorem
(hp : ∀ ⦃a b x⦄, a ≤ x → x ≤ b → p a → p b → p x) : (Ioc a b).map (Embedding.subtype p) = (Ioc a b : Finset α)
Full source 
theorem map_subtype_embedding_Ioc (hp : ∀ ⦃a b x⦄, a ≤ x → x ≤ b → p a → p b → p x):
    (Ioc a b).map (Embedding.subtype p) = (Ioc a b : Finset α) := by
  rw [subtype_Ioc_eq]
  refine Finset.subtype_map_of_mem fun x hx => ?_
  rw [mem_Ioc] at hx
  exact hp hx.1.le hx.2 a.prop b.prop
Subtype Embedding Preserves Open-Closed Interval Finset under Hereditary Predicate
Informal description
Let $\alpha$ be a locally finite order and $p$ a predicate on $\alpha$ satisfying the property that for any $a, b, x \in \alpha$, if $a \leq x \leq b$ and $p(a)$ and $p(b)$ hold, then $p(x)$ also holds. Then the image of the open-closed interval $\text{Ioc}(a, b)$ under the subtype embedding $\{x \in \alpha \mid p(x)\} \hookrightarrow \alpha$ is equal to the finset $\text{Ioc}(a, b)$ in $\alpha$.
Finset.map_subtype_embedding_Ioo theorem
(hp : ∀ ⦃a b x⦄, a ≤ x → x ≤ b → p a → p b → p x) : (Ioo a b).map (Embedding.subtype p) = (Ioo a b : Finset α)
Full source 
theorem map_subtype_embedding_Ioo (hp : ∀ ⦃a b x⦄, a ≤ x → x ≤ b → p a → p b → p x):
    (Ioo a b).map (Embedding.subtype p) = (Ioo a b : Finset α) := by
  rw [subtype_Ioo_eq]
  refine Finset.subtype_map_of_mem fun x hx => ?_
  rw [mem_Ioo] at hx
  exact hp hx.1.le hx.2.le a.prop b.prop
Subtype Embedding Preserves Open Interval Finset: $\text{Ioo}(a, b).\text{map}(p) = \text{Ioo}(a, b)$
Informal description
Let $\alpha$ be a locally finite order with a predicate $p$ on $\alpha$ such that for any $a, b, x \in \alpha$, if $a \leq x \leq b$ and $p(a)$ and $p(b)$ hold, then $p(x)$ also holds. Then the image of the open interval finset $\text{Ioo}(a, b)$ under the subtype embedding $\{x \in \alpha \mid p(x)\} \hookrightarrow \alpha$ is equal to the finset $\text{Ioo}(a, b)$ in $\alpha$.
Finset.subtype_Ici_eq theorem
: Ici a = (Ici (a : α)).subtype p
Full source 
theorem subtype_Ici_eq : Ici a = (Ici (a : α)).subtype p :=
  rfl
Subtype Closed Infinite Interval Equals Subtype of Parent Interval
Informal description
For a subtype $\{x \in \alpha \mid p(x)\}$ of a locally finite order $\alpha$ with finite intervals bounded below, the closed infinite interval $\text{Ici}(a)$ in the subtype is equal to the subtype of the closed infinite interval $\text{Ici}(a)$ in $\alpha$, i.e., \[ \text{Ici}(a) = \{x \in \text{Ici}(a) \mid p(x)\}. \]
Finset.subtype_Ioi_eq theorem
: Ioi a = (Ioi (a : α)).subtype p
Full source 
theorem subtype_Ioi_eq : Ioi a = (Ioi (a : α)).subtype p :=
  rfl
Subtype Open Infinite Interval Equals Subtype of Parent Interval
Informal description
For a subtype $\{x \in \alpha \mid p(x)\}$ of a locally finite order $\alpha$ with finite intervals bounded below, the open infinite interval $\text{Ioi}(a)$ in the subtype is equal to the subtype of the open infinite interval $\text{Ioi}(a)$ in $\alpha$, i.e., \[ \text{Ioi}(a) = \{x \in \text{Ioi}(a) \mid p(x)\}. \]
Finset.map_subtype_embedding_Ici theorem
(hp : ∀ ⦃a x⦄, a ≤ x → p a → p x) : (Ici a).map (Embedding.subtype p) = (Ici a : Finset α)
Full source 
theorem map_subtype_embedding_Ici (hp : ∀ ⦃a x⦄, a ≤ x → p a → p x) :
    (Ici a).map (Embedding.subtype p) = (Ici a : Finset α) := by
  rw [subtype_Ici_eq]
  exact Finset.subtype_map_of_mem fun x hx => hp (mem_Ici.1 hx) a.prop
Subtype Embedding Preserves Closed-Infinite Interval under Monotonicity Condition
Informal description
Let $\alpha$ be a preorder with a locally finite order structure where intervals bounded below are finite, and let $p$ be a predicate on $\alpha$ such that for any $a, x \in \alpha$, if $a \leq x$ and $p(a)$ holds, then $p(x)$ also holds. Then, the image of the closed-infinite interval $\text{Ici}(a)$ under the subtype embedding map is equal to the closed-infinite interval $\text{Ici}(a)$ in $\alpha$ restricted to elements satisfying $p$.
Finset.map_subtype_embedding_Ioi theorem
(hp : ∀ ⦃a x⦄, a ≤ x → p a → p x) : (Ioi a).map (Embedding.subtype p) = (Ioi a : Finset α)
Full source 
theorem map_subtype_embedding_Ioi (hp : ∀ ⦃a x⦄, a ≤ x → p a → p x) :
    (Ioi a).map (Embedding.subtype p) = (Ioi a : Finset α) := by
  rw [subtype_Ioi_eq]
  exact Finset.subtype_map_of_mem fun x hx => hp (mem_Ioi.1 hx).le a.prop
Subtype Embedding Preserves Open-Infinite Interval under Monotonicity Condition
Informal description
Let $\alpha$ be a preorder with a locally finite order structure where intervals bounded below are finite, and let $p$ be a predicate on $\alpha$ such that for any $a, x \in \alpha$, if $a \leq x$ and $p(a)$ holds, then $p(x)$ also holds. Then, for any $a \in \alpha$, the image of the open-infinite interval $\text{Ioi}(a)$ under the subtype embedding map is equal to the open-infinite interval $\text{Ioi}(a)$ in $\alpha$ itself, i.e., \[ \text{map} (\text{Embedding.subtype } p) (\text{Ioi}(a)) = \text{Ioi}(a). \]
Finset.subtype_Iic_eq theorem
: Iic a = (Iic (a : α)).subtype p
Full source 
theorem subtype_Iic_eq : Iic a = (Iic (a : α)).subtype p :=
  rfl
Subtype Lower-Closed Interval Equality
Informal description
For any element $a$ in a subtype defined by a predicate $p$ of a preorder $\alpha$ with finite lower-bounded intervals, the finset $\text{Iic}(a)$ (elements of the subtype less than or equal to $a$) is equal to the finset obtained by taking the subtype of $\text{Iic}(a)$ in $\alpha$ (elements of $\alpha$ less than or equal to $a$) restricted to those elements satisfying $p$.
Finset.subtype_Iio_eq theorem
: Iio a = (Iio (a : α)).subtype p
Full source 
theorem subtype_Iio_eq : Iio a = (Iio (a : α)).subtype p :=
  rfl
Subtype Open Lower Interval Equality
Informal description
For an element $a$ in a subtype defined by a predicate $p$ of a preorder $\alpha$ with finite lower-bounded intervals, the finset $\text{Iio}(a)$ (elements of the subtype less than $a$) is equal to the finset obtained by taking the subtype of $\text{Iio}(a)$ in $\alpha$ (elements of $\alpha$ less than $a$) restricted to those elements satisfying $p$.
Finset.map_subtype_embedding_Iic theorem
(hp : ∀ ⦃a x⦄, x ≤ a → p a → p x) : (Iic a).map (Embedding.subtype p) = (Iic a : Finset α)
Full source 
theorem map_subtype_embedding_Iic (hp : ∀ ⦃a x⦄, x ≤ a → p a → p x) :
    (Iic a).map (Embedding.subtype p) = (Iic a : Finset α) := by
  rw [subtype_Iic_eq]
  exact Finset.subtype_map_of_mem fun x hx => hp (mem_Iic.1 hx) a.prop
Subtype Embedding Preserves Lower-Closed Interval Finset under Downward-Closed Predicate
Informal description
Let $\alpha$ be a preorder with a locally finite order structure for lower-bounded intervals, and let $p$ be a predicate on $\alpha$ satisfying the property that for any elements $a$ and $x$ in $\alpha$, if $x \leq a$ and $p(a)$ holds, then $p(x)$ also holds. Then, for any element $a$ in the subtype defined by $p$, the image of the finset $\text{Iic}(a)$ (elements of the subtype less than or equal to $a$) under the subtype embedding is equal to the finset $\text{Iic}(a)$ in $\alpha$ (elements of $\alpha$ less than or equal to $a$).
Finset.map_subtype_embedding_Iio theorem
(hp : ∀ ⦃a x⦄, x ≤ a → p a → p x) : (Iio a).map (Embedding.subtype p) = (Iio a : Finset α)
Full source 
theorem map_subtype_embedding_Iio (hp : ∀ ⦃a x⦄, x ≤ a → p a → p x) :
    (Iio a).map (Embedding.subtype p) = (Iio a : Finset α) := by
  rw [subtype_Iio_eq]
  exact Finset.subtype_map_of_mem fun x hx => hp (mem_Iio.1 hx).le a.prop
Subtype Embedding Preserves Open Lower Interval Finset under Downward-Closed Predicate
Informal description
Let $\alpha$ be a preorder with a locally finite order structure for lower-bounded intervals, and let $p$ be a predicate on $\alpha$ satisfying the property that for any $a, x \in \alpha$, if $x \leq a$ and $p(a)$ holds, then $p(x)$ holds. Then, for any element $a$ in the subtype defined by $p$, the image of the finset $\text{Iio}(a)$ under the embedding of the subtype into $\alpha$ is equal to the finset $\text{Iio}(a)$ in $\alpha$.
BddBelow.finite_of_bddAbove theorem
[Preorder α] [LocallyFiniteOrder α] {s : Set α} (h₀ : BddBelow s) (h₁ : BddAbove s) : s.Finite
Full source 
theorem BddBelow.finite_of_bddAbove [Preorder α] [LocallyFiniteOrder α]
    {s : Set α} (h₀ : BddBelow s) (h₁ : BddAbove s) :
    s.Finite :=
  let ⟨a, ha⟩ := h₀
  let ⟨b, hb⟩ := h₁
  (Set.finite_Icc a b).subset fun _x hx ↦ ⟨ha hx, hb hx⟩
Finiteness of Bounded Subsets in Locally Finite Orders
Informal description
Let $\alpha$ be a preorder with a locally finite order structure. For any subset $s \subseteq \alpha$ that is bounded below and bounded above, $s$ is finite.
Set.finite_iff_bddAbove theorem
[SemilatticeSup α] [LocallyFiniteOrder α] [OrderBot α] : s.Finite ↔ BddAbove s
Full source 
theorem Set.finite_iff_bddAbove [SemilatticeSup α] [LocallyFiniteOrder α] [OrderBot α] :
    s.Finite ↔ BddAbove s :=
  ⟨fun h ↦ ⟨h.toFinset.sup id, fun _ hx ↦ Finset.le_sup (f := id) ((Finite.mem_toFinset h).mpr hx)⟩,
    fun ⟨m, hm⟩ ↦ (Set.finite_Icc ⊥ m).subset (fun _ hx ↦ ⟨bot_le, hm hx⟩)⟩
Finiteness of a Set in a Locally Finite Semilattice Sup with Bottom is Equivalent to Boundedness Above
Informal description
Let $\alpha$ be a semilattice sup with a locally finite order and a bottom element $\bot$. A subset $s \subseteq \alpha$ is finite if and only if it is bounded above.
Set.finite_iff_bddBelow theorem
[SemilatticeInf α] [LocallyFiniteOrder α] [OrderTop α] : s.Finite ↔ BddBelow s
Full source 
theorem Set.finite_iff_bddBelow [SemilatticeInf α] [LocallyFiniteOrder α] [OrderTop α] :
    s.Finite ↔ BddBelow s :=
  finite_iff_bddAbove (α := αᵒᵈ)
Finiteness of a Set in a Locally Finite Semilattice Inf with Top is Equivalent to Boundedness Below
Informal description
Let $\alpha$ be a semilattice inf with a locally finite order and a top element $\top$. A subset $s \subseteq \alpha$ is finite if and only if it is bounded below.
Set.finite_iff_bddBelow_bddAbove theorem
[Nonempty α] [Lattice α] [LocallyFiniteOrder α] : s.Finite ↔ BddBelow s ∧ BddAbove s
Full source 
theorem Set.finite_iff_bddBelow_bddAbove [Nonempty α] [Lattice α] [LocallyFiniteOrder α] :
    s.Finite ↔ BddBelow s ∧ BddAbove s := by
  obtain (rfl | hs) := s.eq_empty_or_nonempty
  · simp only [Set.finite_empty, bddBelow_empty, bddAbove_empty, and_self]
  exact ⟨fun h ↦ ⟨⟨h.toFinset.inf' ((Finite.toFinset_nonempty h).mpr hs) id,
    fun x hx ↦ Finset.inf'_le id ((Finite.mem_toFinset h).mpr hx)⟩,
    ⟨h.toFinset.sup' ((Finite.toFinset_nonempty h).mpr hs) id, fun x hx ↦ Finset.le_sup' id
    ((Finite.mem_toFinset h).mpr hx)⟩⟩,
    fun ⟨h₀, h₁⟩ ↦ BddBelow.finite_of_bddAbove h₀ h₁⟩
Finiteness of a Set in a Locally Finite Lattice is Equivalent to Boundedness Below and Above
Informal description
Let $\alpha$ be a nonempty lattice equipped with a locally finite order structure. A subset $s \subseteq \alpha$ is finite if and only if it is both bounded below and bounded above.
instLocallyFiniteOrderTopSubtypeLeOfDecidableLEOfLocallyFiniteOrder instance
[Preorder α] [DecidableLE α] [LocallyFiniteOrder α] : LocallyFiniteOrderTop { x : α // x ≤ y }
Full source 
instance (priority := low) [Preorder α] [DecidableLE α] [LocallyFiniteOrder α] :
    LocallyFiniteOrderTop { x : α // x ≤ y } where
  finsetIoi a := Finset.Ioc a ⟨y, by rfl⟩
  finsetIci a := Finset.Icc a ⟨y, by rfl⟩
  finset_mem_Ici a b := by
    simp only [Finset.mem_Icc, and_iff_left_iff_imp]
    exact fun _ => b.property
  finset_mem_Ioi a b := by
    simp only [Finset.mem_Ioc, and_iff_left_iff_imp]
    exact fun _ => b.property
Locally Finite Order Structure on Non-strict Lower Subtype
Informal description
For any preorder $\alpha$ with a decidable order relation and a locally finite order structure, the subtype $\{x \in \alpha \mid x \leq y\}$ for any fixed $y \in \alpha$ forms a locally finite order with finite intervals bounded below. This means that for any element $a$ in this subtype, the interval $[a, \infty)$ is finite.
instLocallyFiniteOrderTopSubtypeLtOfDecidableLTOfLocallyFiniteOrder instance
[Preorder α] [DecidableLT α] [LocallyFiniteOrder α] : LocallyFiniteOrderTop { x : α // x < y }
Full source 
instance (priority := low) [Preorder α] [DecidableLT α] [LocallyFiniteOrder α] :
    LocallyFiniteOrderTop { x : α // x < y } where
  finsetIoi a := (Finset.Ioo ↑a y).subtype _
  finsetIci a := (Finset.Ico ↑a y).subtype _
  finset_mem_Ici a b := by
    simp only [Finset.mem_subtype, Finset.mem_Ico, Subtype.coe_le_coe, and_iff_left_iff_imp]
    exact fun _ => b.property
  finset_mem_Ioi a b := by
    simp only [Finset.mem_subtype, Finset.mem_Ioo, Subtype.coe_lt_coe, and_iff_left_iff_imp]
    exact fun _ => b.property
Locally Finite Order Structure on Strict Subtype
Informal description
For any preorder $\alpha$ with a decidable strict order relation and a locally finite order structure, the subtype $\{x \in \alpha \mid x < y\}$ for any fixed $y \in \alpha$ forms a locally finite order with finite intervals bounded below. This means that for any element $a$ in this subtype, the interval $[a, \infty)$ is finite.
instLocallyFiniteOrderBotSubtypeLeOfDecidableLEOfLocallyFiniteOrder instance
[Preorder α] [DecidableLE α] [LocallyFiniteOrder α] : LocallyFiniteOrderBot { x : α // y ≤ x }
Full source 
instance (priority := low) [Preorder α] [DecidableLE α] [LocallyFiniteOrder α] :
    LocallyFiniteOrderBot { x : α // y ≤ x } where
  finsetIio a := Finset.Ico ⟨y, by rfl⟩ a
  finsetIic a := Finset.Icc ⟨y, by rfl⟩ a
  finset_mem_Iic a b := by
    simp only [Finset.mem_Icc, and_iff_right_iff_imp]
    exact fun _ => b.property
  finset_mem_Iio a b := by
    simp only [Finset.mem_Ico, and_iff_right_iff_imp]
    exact fun _ => b.property
Locally Finite Order Structure on Non-strict Upper Subtype
Informal description
For any preorder $\alpha$ with a decidable order relation and a locally finite order structure, the subtype $\{x \in \alpha \mid y \leq x\}$ for any fixed $y \in \alpha$ forms a locally finite order with finite intervals bounded above. This means that for any element $a$ in this subtype, the interval $(-\infty, a]$ is finite.
instLocallyFiniteOrderBotSubtypeLtOfDecidableLTOfLocallyFiniteOrder instance
[Preorder α] [DecidableLT α] [LocallyFiniteOrder α] : LocallyFiniteOrderBot { x : α // y < x }
Full source 
instance (priority := low) [Preorder α] [DecidableLT α] [LocallyFiniteOrder α] :
    LocallyFiniteOrderBot { x : α // y < x } where
  finsetIio a := (Finset.Ioo y ↑a).subtype _
  finsetIic a := (Finset.Ioc y ↑a).subtype _
  finset_mem_Iic a b := by
    simp only [Finset.mem_subtype, Finset.mem_Ioc, Subtype.coe_le_coe, and_iff_right_iff_imp]
    exact fun _ => b.property
  finset_mem_Iio a b := by
    simp only [Finset.mem_subtype, Finset.mem_Ioo, Subtype.coe_lt_coe, and_iff_right_iff_imp]
    exact fun _ => b.property
Locally Finite Order Structure on Strict Upper Subtype
Informal description
For any preorder $\alpha$ with a decidable strict order relation and a locally finite order structure, the subtype $\{x \in \alpha \mid y < x\}$ for any fixed $y \in \alpha$ forms a locally finite order with finite intervals bounded below. This means that for any element $a$ in this subtype, the interval $(-\infty, a]$ is finite.
instFiniteSubtypeLeOfLocallyFiniteOrderBot instance
[Preorder α] [LocallyFiniteOrderBot α] : Finite { x : α // x ≤ y }
Full source 
instance [Preorder α] [LocallyFiniteOrderBot α] : Finite { x : α // x ≤ y } := by
  simpa only  [coe_Iic] using (Finset.Iic y).finite_toSet
Finiteness of Lower-Bounded Subtype in Locally Finite Order with Bottom
Informal description
For any preorder $\alpha$ with a locally finite order structure where all lower-bounded intervals are finite, the subtype $\{x \in \alpha \mid x \leq y\}$ is finite for any $y \in \alpha$.
instFiniteSubtypeLtOfLocallyFiniteOrderBot instance
[Preorder α] [LocallyFiniteOrderBot α] : Finite { x : α // x < y }
Full source 
instance [Preorder α] [LocallyFiniteOrderBot α] : Finite { x : α // x < y } := by
  simpa only [coe_Iio] using (Finset.Iio y).finite_toSet
Finiteness of Strict Lower Subtype in Locally Finite Order with Bottom
Informal description
For any preorder $\alpha$ that is a locally finite order with finite lower-bounded intervals, the subtype $\{x \in \alpha \mid x < y\}$ is finite for any $y \in \alpha$.
instFiniteSubtypeLeOfLocallyFiniteOrderTop instance
[Preorder α] [LocallyFiniteOrderTop α] : Finite { x : α // y ≤ x }
Full source 
instance [Preorder α] [LocallyFiniteOrderTop α] : Finite { x : α // y ≤ x } := by
  simpa only [coe_Ici] using (Finset.Ici y).finite_toSet
Finiteness of Upper Sets in Locally Finite Orders with Top
Informal description
For any preorder $\alpha$ that is a locally finite order with finite intervals bounded below, and for any element $y \in \alpha$, the set $\{x \in \alpha \mid y \leq x\}$ is finite.
instFiniteSubtypeLtOfLocallyFiniteOrderTop instance
[Preorder α] [LocallyFiniteOrderTop α] : Finite { x : α // y < x }
Full source 
instance [Preorder α] [LocallyFiniteOrderTop α] : Finite { x : α // y < x } := by
  simpa only [coe_Ioi] using (Finset.Ioi y).finite_toSet
Finiteness of Strict Upper Sets in Locally Finite Orders with Top
Informal description
For any preorder $\alpha$ that is a locally finite order with finite intervals bounded below, and for any element $y \in \alpha$, the set $\{x \in \alpha \mid y < x\}$ is finite.
Set.toFinset_Icc theorem
(a b : α) [Fintype (Icc a b)] : (Icc a b).toFinset = Finset.Icc a b
Full source 
@[simp] lemma toFinset_Icc (a b : α) [Fintype (Icc a b)] : (Icc a b).toFinset = Finset.Icc a b := by
  ext; simp
Equality of Finset and Set Representations for Closed Interval in Locally Finite Orders
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the finite set representation of the closed interval $[a, b]$ as a finset is equal to the finset obtained by converting the set $[a, b]$ to a finset. In other words, $\text{toFinset}([a, b]) = \text{Icc}(a, b)$.
Set.toFinset_Ico theorem
(a b : α) [Fintype (Ico a b)] : (Ico a b).toFinset = Finset.Ico a b
Full source 
@[simp] lemma toFinset_Ico (a b : α) [Fintype (Ico a b)] : (Ico a b).toFinset = Finset.Ico a b := by
  ext; simp
Equality of Finset and Set Representations for Closed-Open Interval in Locally Finite Orders
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the finite set representation of the interval $[a, b)$ as a finset is equal to the finset obtained by converting the set $[a, b)$ to a finset. In other words, $\text{toFinset}([a, b)) = \text{Ico}(a, b)$.
Set.toFinset_Ioc theorem
(a b : α) [Fintype (Ioc a b)] : (Ioc a b).toFinset = Finset.Ioc a b
Full source 
@[simp] lemma toFinset_Ioc (a b : α) [Fintype (Ioc a b)] : (Ioc a b).toFinset = Finset.Ioc a b := by
  ext; simp
Equality of Set and Finset Representations for Open-Closed Interval $(a, b]$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the finset obtained by converting the set $\text{Ioc}(a, b) = \{x \in \alpha \mid a < x \leq b\}$ to a finset is equal to the finset $\text{Finset.Ioc}(a, b)$.
Set.toFinset_Ioo theorem
(a b : α) [Fintype (Ioo a b)] : (Ioo a b).toFinset = Finset.Ioo a b
Full source 
@[simp] lemma toFinset_Ioo (a b : α) [Fintype (Ioo a b)] : (Ioo a b).toFinset = Finset.Ioo a b := by
  ext; simp
Equality of Set and Finset Representations for Open Interval $(a, b)$
Informal description
For any elements $a$ and $b$ in a locally finite order $\alpha$, the finset obtained by converting the open interval $(a, b) = \{x \in \alpha \mid a < x < b\}$ to a finset is equal to the finset $\text{Ioo}(a, b)$.
Set.toFinset_Ici theorem
(a : α) [Fintype (Ici a)] : (Ici a).toFinset = Finset.Ici a
Full source 
@[simp]
lemma toFinset_Ici (a : α) [Fintype (Ici a)] : (Ici a).toFinset = Finset.Ici a := by ext; simp
Equality of Set and Finset Representations of Closed Infinite Interval $[a, \infty)$
Informal description
For any element $a$ in a preorder $\alpha$ where the closed infinite interval $[a, \infty)$ is finite, the finset obtained by converting the set $\text{Ici}(a) = \{x \in \alpha \mid a \leq x\}$ to a finset is equal to the finset $\text{Finset.Ici}(a)$.
Set.toFinset_Ioi theorem
(a : α) [Fintype (Ioi a)] : (Ioi a).toFinset = Finset.Ioi a
Full source 
@[simp]
lemma toFinset_Ioi (a : α) [Fintype (Ioi a)] : (Ioi a).toFinset = Finset.Ioi a := by ext; simp
Equality of Set and Finset Representations of Open Infinite Interval $(a, \infty)$
Informal description
For any element $a$ in a preorder $\alpha$ where the open infinite interval $(a, \infty)$ is finite, the finset obtained by converting the set $\text{Ioi}(a) = \{x \in \alpha \mid a < x\}$ to a finset is equal to the finset $\text{Finset.Ioi}(a)$.
Set.toFinset_Iic theorem
(a : α) [Fintype (Iic a)] : (Iic a).toFinset = Finset.Iic a
Full source 
@[simp]
lemma toFinset_Iic (a : α) [Fintype (Iic a)] : (Iic a).toFinset = Finset.Iic a := by ext; simp
Equality of Set and Finset Representations of Closed Infinite Interval $(-\infty, a]$
Informal description
For any element $a$ in a preorder $\alpha$ where the closed infinite interval $(-\infty, a]$ is finite, the finset obtained by converting the set $\text{Iic}(a) = \{x \in \alpha \mid x \leq a\}$ to a finset is equal to the finset $\text{Finset.Iic}(a)$.
Set.toFinset_Iio theorem
(a : α) [Fintype (Iio a)] : (Iio a).toFinset = Finset.Iio a
Full source 
@[simp]
lemma toFinset_Iio (a : α) [Fintype (Iio a)] : (Iio a).toFinset = Finset.Iio a := by ext; simp
Equality of Set and Finset Representations of Open Lower Interval $(-\infty, a)$
Informal description
For any element $a$ in a preorder $\alpha$ where the left-infinite right-open interval $(-\infty, a)$ is finite, the finset obtained by converting the set $\text{Iio}(a) = \{x \in \alpha \mid x < a\}$ to a finset is equal to the finset $\text{Finset.Iio}(a)$.
LocallyFiniteOrder.ofOrderIsoClass abbrev
{F M N : Type*} [Preorder M] [Preorder N] [EquivLike F M N] [OrderIsoClass F M N] (f : F) [LocallyFiniteOrder N] : LocallyFiniteOrder M
Full source 
/-- A `LocallyFiniteOrder` can be transferred across an order isomorphism. -/
-- See note [reducible non instances]
abbrev LocallyFiniteOrder.ofOrderIsoClass {F M N : Type*} [Preorder M] [Preorder N]
    [EquivLike F M N] [OrderIsoClass F M N] (f : F) [LocallyFiniteOrder N] :
    LocallyFiniteOrder M where
  finsetIcc x y := (finsetIcc (f x) (f y)).map ⟨EquivLike.inv f, (EquivLike.right_inv f).injective⟩
  finsetIco x y := (finsetIco (f x) (f y)).map ⟨EquivLike.inv f, (EquivLike.right_inv f).injective⟩
  finsetIoc x y := (finsetIoc (f x) (f y)).map ⟨EquivLike.inv f, (EquivLike.right_inv f).injective⟩
  finsetIoo x y := (finsetIoo (f x) (f y)).map ⟨EquivLike.inv f, (EquivLike.right_inv f).injective⟩
  finset_mem_Icc := by simp [finset_mem_Icc, EquivLike.inv_apply_eq_iff_eq_apply]
  finset_mem_Ico := by
    simp [finset_mem_Ico, EquivLike.inv_apply_eq_iff_eq_apply, map_lt_map_iff]
  finset_mem_Ioc := by
    simp [finset_mem_Ioc, EquivLike.inv_apply_eq_iff_eq_apply, map_lt_map_iff]
  finset_mem_Ioo := by
    simp [finset_mem_Ioo, EquivLike.inv_apply_eq_iff_eq_apply, map_lt_map_iff]
Transfer of Locally Finite Order via Order Isomorphism
Informal description
Given two preordered types $M$ and $N$, and a type $F$ of order isomorphisms between $M$ and $N$ (i.e., bijective order-preserving maps), if $N$ is a locally finite order, then $M$ inherits a locally finite order structure via any order isomorphism $f : F$. More precisely, for any order isomorphism $f : M \to N$ and any $a, b \in M$, the interval $[a, b]$ in $M$ is finite because its image under $f$ is the interval $[f(a), f(b)]$ in $N$, which is finite by the locally finite order property of $N$.