# mathlibdocumentation

order.locally_finite

# Locally finite orders #

This file defines locally finite orders.

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

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

## Examples #

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

## Main declarations #

In a locally_finite_order,

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

In a locally_finite_order_top,

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

In a locally_finite_order_bot,

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

## Instances #

A locally_finite_order instance can be built

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

Instances for concrete types are proved in their respective files:

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

## TODO #

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

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

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

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

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


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

@[class]
structure locally_finite_order (α : Type u_1) [preorder α] :
Type u_1
• finset_Icc : α → α →
• finset_Ico : α → α →
• finset_Ioc : α → α →
• finset_Ioo : α → α →
• finset_mem_Icc : ∀ (a b x : α), a x x b
• finset_mem_Ico : ∀ (a b x : α), a x x < b
• finset_mem_Ioc : ∀ (a b x : α), a < x x b
• finset_mem_Ioo : ∀ (a b x : α), a < x x < b

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Equations
@[protected, reducible]
def is_empty.to_locally_finite_order {α : Type u_1} [preorder α] [is_empty α] :

An empty type is locally finite.

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

Equations
@[protected, reducible]
def is_empty.to_locally_finite_order_top {α : Type u_1} [preorder α] [is_empty α] :

An empty type is locally finite.

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

Equations
@[protected, reducible]
def is_empty.to_locally_finite_order_bot {α : Type u_1} [preorder α] [is_empty α] :

An empty type is locally finite.

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

Equations

### Intervals as finsets #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

### Intervals as multisets #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

### Finiteness of set intervals #

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

### Instances #

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

A noncomputable constructor from the finiteness of all closed intervals.

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

A fintype is a locally finite order.

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

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

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

Equations
@[protected, instance]
def order_dual.locally_finite_order {α : Type u_1} [preorder α]  :

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

lemma this : (Icc (to_dual (to_dual a)) (to_dual (to_dual b)) : _) = (Icc a b : _) := rfl

Equations
theorem Icc_to_dual {α : Type u_1} [preorder α] (a b : α) :
theorem Ico_to_dual {α : Type u_1} [preorder α] (a b : α) :
theorem Ioc_to_dual {α : Type u_1} [preorder α] (a b : α) :
theorem Ioo_to_dual {α : Type u_1} [preorder α] (a b : α) :
theorem Icc_of_dual {α : Type u_1} [preorder α] (a b : αᵒᵈ) :
theorem Ico_of_dual {α : Type u_1} [preorder α] (a b : αᵒᵈ) :
theorem Ioc_of_dual {α : Type u_1} [preorder α] (a b : αᵒᵈ) :
theorem Ioo_of_dual {α : Type u_1} [preorder α] (a b : αᵒᵈ) :
@[protected, instance]
def order_dual.locally_finite_order_bot {α : Type u_1} [preorder α]  :

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

lemma this : (Iic (to_dual (to_dual a)) : _) = (Iic a : _) := rfl

Equations
theorem Iic_to_dual {α : Type u_1} [preorder α] (a : α) :
theorem Iio_to_dual {α : Type u_1} [preorder α] (a : α) :
theorem Ici_of_dual {α : Type u_1} [preorder α] (a : αᵒᵈ) :
theorem Ioi_of_dual {α : Type u_1} [preorder α] (a : αᵒᵈ) :
@[protected, instance]
def order_dual.locally_finite_order_top {α : Type u_1} [preorder α]  :

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

lemma this : (Ici (to_dual (to_dual a)) : _) = (Ici a : _) := rfl

Equations
theorem Ici_to_dual {α : Type u_1} [preorder α] (a : α) :
theorem Ioi_to_dual {α : Type u_1} [preorder α] (a : α) :
theorem Iic_of_dual {α : Type u_1} [preorder α] (a : αᵒᵈ) :
theorem Iio_of_dual {α : Type u_1} [preorder α] (a : αᵒᵈ) :
@[protected, instance]
def prod.locally_finite_order {α : Type u_1} {β : Type u_2} [preorder α] [preorder β]  :
Equations
@[protected, instance]
def prod.locally_finite_order_top {α : Type u_1} {β : Type u_2} [preorder α] [preorder β]  :
Equations
@[protected, instance]
def prod.locally_finite_order_bot {α : Type u_1} {β : Type u_2} [preorder α] [preorder β]  :
Equations

#### with_top, with_bot#

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

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

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

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

Transfer locally_finite_order across an order_iso.

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

Transfer locally_finite_order_top across an order_iso.

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

Transfer locally_finite_order_bot across an order_iso.

Equations

#### Subtype of a locally finite order #

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