# Intervals as finsets #

This file provides basic results about all the `Finset.Ixx`, which are defined in `Order.Interval.Finset.Defs`.

In addition, it shows that in a locally finite order `≤` and `<` are the transitive closures of, respectively, `⩿` and `⋖`, which then leads to a characterization of monotone and strictly functions whose domain is a locally finite order. In particular, this file proves:

- `le_iff_transGen_wcovBy`: `≤` is the transitive closure of `⩿`
- `lt_iff_transGen_covBy`: `<` is the transitive closure of `⋖`
- `monotone_iff_forall_wcovBy`: Characterization of monotone functions
- `strictMono_iff_forall_covBy`: Characterization of strictly monotone functions

## TODO #

This file was originally only about `Finset.Ico a b` where `a b : ℕ`. No care has yet been taken to generalize these lemmas properly and many lemmas about `Icc`, `Ioc`, `Ioo` are missing. In general, what's to do is taking the lemmas in `Data.X.Intervals` and abstract away the concrete structure.

Complete the API. See https://github.com/leanprover-community/mathlib/pull/14448#discussion_r906109235 for some ideas.

source
@[simp]
theorem Finset.nonempty_Icc {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
(Icc a b).Nonempty ↔ a ≤ b
source
theorem Finset.Aesop.nonempty_Icc_of_le {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
a ≤ b → (Icc a b).Nonempty

Alias of the reverse direction of `Finset.nonempty_Icc`.

source
@[simp]
theorem Finset.nonempty_Ico {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
(Ico a b).Nonempty ↔ a < b
source
theorem Finset.Aesop.nonempty_Ico_of_lt {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
a < b → (Ico a b).Nonempty

Alias of the reverse direction of `Finset.nonempty_Ico`.

source
@[simp]
theorem Finset.nonempty_Ioc {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
(Ioc a b).Nonempty ↔ a < b
source
theorem Finset.Aesop.nonempty_Ioc_of_lt {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
a < b → (Ioc a b).Nonempty

Alias of the reverse direction of `Finset.nonempty_Ioc`.

source
@[simp]
theorem Finset.nonempty_Ioo {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] [DenselyOrdered α] :
(Ioo a b).Nonempty ↔ a < b
source
@[simp]
theorem Finset.Icc_eq_empty_iff {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
Icc a b = ∅ ↔ ¬a ≤ b
source
@[simp]
theorem Finset.Ico_eq_empty_iff {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
Ico a b = ∅ ↔ ¬a < b
source
@[simp]
theorem Finset.Ioc_eq_empty_iff {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
Ioc a b = ∅ ↔ ¬a < b
source
@[simp]
theorem Finset.Ioo_eq_empty_iff {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] [DenselyOrdered α] :
Ioo a b = ∅ ↔ ¬a < b
source
theorem Finset.Icc_eq_empty {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
¬a ≤ b → Icc a b = ∅

Alias of the reverse direction of `Finset.Icc_eq_empty_iff`.

source
theorem Finset.Ico_eq_empty {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
¬a < b → Ico a b = ∅

Alias of the reverse direction of `Finset.Ico_eq_empty_iff`.

source
theorem Finset.Ioc_eq_empty {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
¬a < b → Ioc a b = ∅

Alias of the reverse direction of `Finset.Ioc_eq_empty_iff`.

source
@[simp]
theorem Finset.Ioo_eq_empty {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] (h : ¬a < b) :
Ioo a b = ∅
source
@[simp]
theorem Finset.Icc_eq_empty_of_lt {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] (h : b < a) :
Icc a b = ∅
source
@[simp]
theorem Finset.Ico_eq_empty_of_le {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] (h : b ≤ a) :
Ico a b = ∅
source
@[simp]
theorem Finset.Ioc_eq_empty_of_le {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] (h : b ≤ a) :
Ioc a b = ∅
source
@[simp]
theorem Finset.Ioo_eq_empty_of_le {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] (h : b ≤ a) :
Ioo a b = ∅
source
theorem Finset.left_mem_Icc {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
a ∈ Icc a b ↔ a ≤ b
source
theorem Finset.left_mem_Ico {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
a ∈ Ico a b ↔ a < b
source
theorem Finset.right_mem_Icc {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
b ∈ Icc a b ↔ a ≤ b
source
theorem Finset.right_mem_Ioc {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
b ∈ Ioc a b ↔ a < b
source
theorem Finset.left_notMem_Ioc {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
a ∉ Ioc a b
source
@[deprecated Finset.left_notMem_Ioc (since := "2025-05-23")]
theorem Finset.left_not_mem_Ioc {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
a ∉ Ioc a b

Alias of `Finset.left_notMem_Ioc`.

source
theorem Finset.left_notMem_Ioo {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
a ∉ Ioo a b
source
@[deprecated Finset.left_notMem_Ioo (since := "2025-05-23")]
theorem Finset.left_not_mem_Ioo {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
a ∉ Ioo a b

Alias of `Finset.left_notMem_Ioo`.

source
theorem Finset.right_notMem_Ico {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
b ∉ Ico a b
source
@[deprecated Finset.right_notMem_Ico (since := "2025-05-23")]
theorem Finset.right_not_mem_Ico {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
b ∉ Ico a b

Alias of `Finset.right_notMem_Ico`.

source
theorem Finset.right_notMem_Ioo {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
b ∉ Ioo a b
source
@[deprecated Finset.right_notMem_Ioo (since := "2025-05-23")]
theorem Finset.right_not_mem_Ioo {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
b ∉ Ioo a b

Alias of `Finset.right_notMem_Ioo`.

source
theorem Finset.Icc_subset_Icc {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) :
Icc a₁ b₁ ⊆ Icc a₂ b₂
source
theorem Finset.Ico_subset_Ico {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) :
Ico a₁ b₁ ⊆ Ico a₂ b₂
source
theorem Finset.Ioc_subset_Ioc {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) :
Ioc a₁ b₁ ⊆ Ioc a₂ b₂
source
theorem Finset.Ioo_subset_Ioo {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) :
Ioo a₁ b₁ ⊆ Ioo a₂ b₂
source
theorem Finset.Icc_subset_Icc_left {α : Type u_2} {a₁ a₂ b : α} [Preorder α] [LocallyFiniteOrder α] (h : a₁ ≤ a₂) :
Icc a₂ b ⊆ Icc a₁ b
source
theorem Finset.Ico_subset_Ico_left {α : Type u_2} {a₁ a₂ b : α} [Preorder α] [LocallyFiniteOrder α] (h : a₁ ≤ a₂) :
Ico a₂ b ⊆ Ico a₁ b
source
theorem Finset.Ioc_subset_Ioc_left {α : Type u_2} {a₁ a₂ b : α} [Preorder α] [LocallyFiniteOrder α] (h : a₁ ≤ a₂) :
Ioc a₂ b ⊆ Ioc a₁ b
source
theorem Finset.Ioo_subset_Ioo_left {α : Type u_2} {a₁ a₂ b : α} [Preorder α] [LocallyFiniteOrder α] (h : a₁ ≤ a₂) :
Ioo a₂ b ⊆ Ioo a₁ b
source
theorem Finset.Icc_subset_Icc_right {α : Type u_2} {a b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (h : b₁ ≤ b₂) :
Icc a b₁ ⊆ Icc a b₂
source
theorem Finset.Ico_subset_Ico_right {α : Type u_2} {a b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (h : b₁ ≤ b₂) :
Ico a b₁ ⊆ Ico a b₂
source
theorem Finset.Ioc_subset_Ioc_right {α : Type u_2} {a b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (h : b₁ ≤ b₂) :
Ioc a b₁ ⊆ Ioc a b₂
source
theorem Finset.Ioo_subset_Ioo_right {α : Type u_2} {a b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (h : b₁ ≤ b₂) :
Ioo a b₁ ⊆ Ioo a b₂
source
theorem Finset.Ico_subset_Ioo_left {α : Type u_2} {a₁ a₂ b : α} [Preorder α] [LocallyFiniteOrder α] (h : a₁ < a₂) :
Ico a₂ b ⊆ Ioo a₁ b
source
theorem Finset.Ioc_subset_Ioo_right {α : Type u_2} {a b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (h : b₁ < b₂) :
Ioc a b₁ ⊆ Ioo a b₂
source
theorem Finset.Icc_subset_Ico_right {α : Type u_2} {a b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (h : b₁ < b₂) :
Icc a b₁ ⊆ Ico a b₂
source
theorem Finset.Ioo_subset_Ico_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
Ioo a b ⊆ Ico a b
source
theorem Finset.Ioo_subset_Ioc_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
Ioo a b ⊆ Ioc a b
source
theorem Finset.Ico_subset_Icc_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
Ico a b ⊆ Icc a b
source
theorem Finset.Ioc_subset_Icc_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
Ioc a b ⊆ Icc a b
source
theorem Finset.Ioo_subset_Icc_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] :
Ioo a b ⊆ Icc a b
source
theorem Finset.Icc_subset_Icc_iff {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (h₁ : a₁ ≤ b₁) :
Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
source
theorem Finset.Icc_subset_Ioo_iff {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (h₁ : a₁ ≤ b₁) :
Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂
source
theorem Finset.Icc_subset_Ico_iff {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (h₁ : a₁ ≤ b₁) :
Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂
source
theorem Finset.Icc_subset_Ioc_iff {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (h₁ : a₁ ≤ b₁) :
Icc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ a₂ < a₁ ∧ b₁ ≤ b₂
source
theorem Finset.Icc_ssubset_Icc_left {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (hI : a₂ ≤ b₂) (ha : a₂ < a₁) (hb : b₁ ≤ b₂) :
Icc a₁ b₁ ⊂ Icc a₂ b₂
source
theorem Finset.Icc_ssubset_Icc_right {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (hI : a₂ ≤ b₂) (ha : a₂ ≤ a₁) (hb : b₁ < b₂) :
Icc a₁ b₁ ⊂ Icc a₂ b₂
source
@[simp]
theorem Finset.Ioc_disjoint_Ioc_of_le {α : Type u_2} {a b c : α} [Preorder α] [LocallyFiniteOrder α] {d : α} (hbc : b ≤ c) :
Disjoint (Ioc a b) (Ioc c d)
source
theorem not_lt_of_denselyOrdered_of_locallyFinite {α : Type u_2} [Preorder α] [LocallyFiniteOrder α] [DenselyOrdered α] (a b : α) :
¬a < b
source
theorem Finset.Ico_self {α : Type u_2} (a : α) [Preorder α] [LocallyFiniteOrder α] :
Ico a a = ∅
source
theorem Finset.Ioc_self {α : Type u_2} (a : α) [Preorder α] [LocallyFiniteOrder α] :
Ioc a a = ∅
source
theorem Finset.Ioo_self {α : Type u_2} (a : α) [Preorder α] [LocallyFiniteOrder α] :
Ioo a a = ∅
source
def Set.fintypeOfMemBounds {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] {s : Set α} [DecidablePred fun (x : α) => x ∈ s] (ha : a ∈ lowerBounds s) (hb : b ∈ upperBounds s) :
Fintype ↑s

A set with upper and lower bounds in a locally finite order is a fintype

Equations

- Set.fintypeOfMemBounds ha hb = (Set.Icc a b).fintypeSubset ⋯

Instances For

source
theorem Finset.Ico_filter_lt_of_le_left {α : Type u_2} {a b c : α} [Preorder α] [LocallyFiniteOrder α] [DecidablePred fun (x : α) => x < c] (hca : c ≤ a) :
{x ∈ Ico a b | x < c} = ∅
source
theorem Finset.Ico_filter_lt_of_right_le {α : Type u_2} {a b c : α} [Preorder α] [LocallyFiniteOrder α] [DecidablePred fun (x : α) => x < c] (hbc : b ≤ c) :
{x ∈ Ico a b | x < c} = Ico a b
source
theorem Finset.Ico_filter_lt_of_le_right {α : Type u_2} {a b c : α} [Preorder α] [LocallyFiniteOrder α] [DecidablePred fun (x : α) => x < c] (hcb : c ≤ b) :
{x ∈ Ico a b | x < c} = Ico a c
source
theorem Finset.Ico_filter_le_of_le_left {α : Type u_2} [Preorder α] [LocallyFiniteOrder α] {a b c : α} [DecidablePred fun (x : α) => c ≤ x] (hca : c ≤ a) :
{x ∈ Ico a b | c ≤ x} = Ico a b
source
theorem Finset.Ico_filter_le_of_right_le {α : Type u_2} [Preorder α] [LocallyFiniteOrder α] {a b : α} [DecidablePred fun (x : α) => b ≤ x] :
{x ∈ Ico a b | b ≤ x} = ∅
source
theorem Finset.Ico_filter_le_of_left_le {α : Type u_2} [Preorder α] [LocallyFiniteOrder α] {a b c : α} [DecidablePred fun (x : α) => c ≤ x] (hac : a ≤ c) :
{x ∈ Ico a b | c ≤ x} = Ico c b
source
theorem Finset.Icc_filter_lt_of_lt_right {α : Type u_2} [Preorder α] [LocallyFiniteOrder α] {a b c : α} [DecidablePred fun (x : α) => x < c] (h : b < c) :
{x ∈ Icc a b | x < c} = Icc a b
source
theorem Finset.Ioc_filter_lt_of_lt_right {α : Type u_2} [Preorder α] [LocallyFiniteOrder α] {a b c : α} [DecidablePred fun (x : α) => x < c] (h : b < c) :
{x ∈ Ioc a b | x < c} = Ioc a b
source
theorem Finset.Iic_filter_lt_of_lt_right {α : Type u_3} [Preorder α] [LocallyFiniteOrderBot α] {a c : α} [DecidablePred fun (x : α) => x < c] (h : a < c) :
{x ∈ Iic a | x < c} = Iic a
source
theorem Finset.filter_lt_lt_eq_Ioo {α : Type u_2} (a b : α) [Preorder α] [LocallyFiniteOrder α] [Fintype α] [DecidablePred fun (j : α) => a < j ∧ j < b] :
{j : α | a < j ∧ j < b} = Ioo a b
source
theorem Finset.filter_lt_le_eq_Ioc {α : Type u_2} (a b : α) [Preorder α] [LocallyFiniteOrder α] [Fintype α] [DecidablePred fun (j : α) => a < j ∧ j ≤ b] :
{j : α | a < j ∧ j ≤ b} = Ioc a b
source
theorem Finset.filter_le_lt_eq_Ico {α : Type u_2} (a b : α) [Preorder α] [LocallyFiniteOrder α] [Fintype α] [DecidablePred fun (j : α) => a ≤ j ∧ j < b] :
{j : α | a ≤ j ∧ j < b} = Ico a b
source
theorem Finset.filter_le_le_eq_Icc {α : Type u_2} (a b : α) [Preorder α] [LocallyFiniteOrder α] [Fintype α] [DecidablePred fun (j : α) => a ≤ j ∧ j ≤ b] :
{j : α | a ≤ j ∧ j ≤ b} = Icc a b
source
@[simp]
theorem Finset.Ioi_eq_empty {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderTop α] :
Ioi a = ∅ ↔ IsMax a
source
@[simp]
theorem IsMax.finsetIoi_eq {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderTop α] :
IsMax a → Finset.Ioi a = ∅

Alias of the reverse direction of `Finset.Ioi_eq_empty`.

source
@[simp]
theorem Finset.Ioi_nonempty {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderTop α] :
(Ioi a).Nonempty ↔ ¬IsMax a
source
theorem Finset.Ioi_top {α : Type u_2} [Preorder α] [LocallyFiniteOrderTop α] [OrderTop α] :
Ioi ⊤ = ∅
source
@[simp]
theorem Finset.Ici_bot {α : Type u_2} [Preorder α] [LocallyFiniteOrderTop α] [OrderBot α] [Fintype α] :
Ici ⊥ = univ
source
@[simp]
theorem Finset.nonempty_Ici {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderTop α] :
(Ici a).Nonempty
source
theorem Finset.nonempty_Ioi {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderTop α] :
(Ioi a).Nonempty ↔ ¬IsMax a
source
theorem Finset.Aesop.nonempty_Ioi_of_not_isMax {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderTop α] :
¬IsMax a → (Ioi a).Nonempty

Alias of the reverse direction of `Finset.nonempty_Ioi`.

source
@[simp]
theorem Finset.Ici_subset_Ici {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderTop α] :
Ici a ⊆ Ici b ↔ b ≤ a
source
theorem GCongr.Finset.Ici_subset_Ici {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderTop α] :
b ≤ a → Finset.Ici a ⊆ Finset.Ici b

Alias of the reverse direction of `Finset.Ici_subset_Ici`.

source
@[simp]
theorem Finset.Ici_ssubset_Ici {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderTop α] :
Ici a ⊂ Ici b ↔ b < a
source
theorem GCongr.Finset.Ici_ssubset_Ici {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderTop α] :
b < a → Finset.Ici a ⊂ Finset.Ici b

Alias of the reverse direction of `Finset.Ici_ssubset_Ici`.

source
theorem Finset.Ioi_subset_Ioi {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderTop α] (h : a ≤ b) :
Ioi b ⊆ Ioi a
source
theorem Finset.Ioi_ssubset_Ioi {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderTop α] (h : a < b) :
Ioi b ⊂ Ioi a
source
theorem Finset.Icc_subset_Ici_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderTop α] [LocallyFiniteOrder α] :
Icc a b ⊆ Ici a
source
theorem Finset.Ico_subset_Ici_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderTop α] [LocallyFiniteOrder α] :
Ico a b ⊆ Ici a
source
theorem Finset.Ioc_subset_Ioi_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderTop α] [LocallyFiniteOrder α] :
Ioc a b ⊆ Ioi a
source
theorem Finset.Ioo_subset_Ioi_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderTop α] [LocallyFiniteOrder α] :
Ioo a b ⊆ Ioi a
source
theorem Finset.Ioc_subset_Ici_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderTop α] [LocallyFiniteOrder α] :
Ioc a b ⊆ Ici a
source
theorem Finset.Ioo_subset_Ici_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderTop α] [LocallyFiniteOrder α] :
Ioo a b ⊆ Ici a
source
@[simp]
theorem Finset.Iio_eq_empty {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderBot α] :
Iio a = ∅ ↔ IsMin a
source
@[simp]
theorem IsMin.finsetIio_eq {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderBot α] :
IsMin a → Finset.Iio a = ∅

Alias of the reverse direction of `Finset.Iio_eq_empty`.

source
@[simp]
theorem Finset.Iio_nonempty {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderBot α] :
(Iio a).Nonempty ↔ ¬IsMin a
source
theorem Finset.Iio_bot {α : Type u_2} [Preorder α] [LocallyFiniteOrderBot α] [OrderBot α] :
Iio ⊥ = ∅
source
@[simp]
theorem Finset.Iic_top {α : Type u_2} [Preorder α] [LocallyFiniteOrderBot α] [OrderTop α] [Fintype α] :
Iic ⊤ = univ
source
@[simp]
theorem Finset.nonempty_Iic {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderBot α] :
(Iic a).Nonempty
source
theorem Finset.nonempty_Iio {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderBot α] :
(Iio a).Nonempty ↔ ¬IsMin a
source
theorem Finset.Aesop.nonempty_Iio_of_not_isMin {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderBot α] :
¬IsMin a → (Iio a).Nonempty

Alias of the reverse direction of `Finset.nonempty_Iio`.

source
@[simp]
theorem Finset.Iic_subset_Iic {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderBot α] :
Iic a ⊆ Iic b ↔ a ≤ b
source
theorem GCongr.Finset.Iic_subset_Iic {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderBot α] :
a ≤ b → Finset.Iic a ⊆ Finset.Iic b

Alias of the reverse direction of `Finset.Iic_subset_Iic`.

source
@[simp]
theorem Finset.Iic_ssubset_Iic {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderBot α] :
Iic a ⊂ Iic b ↔ a < b
source
theorem GCongr.Finset.Iic_ssubset_Iic {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderBot α] :
a < b → Finset.Iic a ⊂ Finset.Iic b

Alias of the reverse direction of `Finset.Iic_ssubset_Iic`.

source
theorem Finset.Iio_subset_Iio {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderBot α] (h : a ≤ b) :
Iio a ⊆ Iio b
source
theorem Finset.Iio_ssubset_Iio {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderBot α] (h : a < b) :
Iio a ⊂ Iio b
source
theorem Finset.Icc_subset_Iic_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderBot α] [LocallyFiniteOrder α] :
Icc a b ⊆ Iic b
source
theorem Finset.Ioc_subset_Iic_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderBot α] [LocallyFiniteOrder α] :
Ioc a b ⊆ Iic b
source
theorem Finset.Ico_subset_Iio_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderBot α] [LocallyFiniteOrder α] :
Ico a b ⊆ Iio b
source
theorem Finset.Ioo_subset_Iio_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderBot α] [LocallyFiniteOrder α] :
Ioo a b ⊆ Iio b
source
theorem Finset.Ico_subset_Iic_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderBot α] [LocallyFiniteOrder α] :
Ico a b ⊆ Iic b
source
theorem Finset.Ioo_subset_Iic_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderBot α] [LocallyFiniteOrder α] :
Ioo a b ⊆ Iic b
source
theorem Finset.Iic_disjoint_Ioc {α : Type u_2} {a b c : α} [Preorder α] [LocallyFiniteOrderBot α] [LocallyFiniteOrder α] (h : a ≤ b) :
Disjoint (Iic a) (Ioc b c)
source
def Equiv.IicFinsetSet {α : Type u_2} [Preorder α] [LocallyFiniteOrderBot α] (a : α) :
↥(Finset.Iic a) ≃ ↑(Set.Iic a)

An equivalence between `Finset.Iic a` and `Set.Iic a`.

Equations

- Equiv.IicFinsetSet a = { toFun := fun (b : ↥(Finset.Iic a)) => ⟨↑b, ⋯⟩, invFun := fun (b : ↑(Set.Iic a)) => ⟨↑b, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
theorem Finset.Ioi_subset_Ici_self {α : Type u_2} [Preorder α] [LocallyFiniteOrderTop α] {a : α} :
Ioi a ⊆ Ici a
source
theorem BddBelow.finite {α : Type u_2} [Preorder α] [LocallyFiniteOrderTop α] {s : Set α} (hs : BddBelow s) :
s.Finite
source
theorem Set.Infinite.not_bddBelow {α : Type u_2} [Preorder α] [LocallyFiniteOrderTop α] {s : Set α} :
s.Infinite → ¬BddBelow s
source
theorem Finset.filter_lt_eq_Ioi {α : Type u_2} [Preorder α] [LocallyFiniteOrderTop α] {a : α} [Fintype α] [DecidablePred fun (x : α) => a < x] :
{x : α | a < x} = Ioi a
source
theorem Finset.filter_le_eq_Ici {α : Type u_2} [Preorder α] [LocallyFiniteOrderTop α] {a : α} [Fintype α] [DecidablePred fun (x : α) => a ≤ x] :
{x : α | a ≤ x} = Ici a
source
theorem Finset.Iio_subset_Iic_self {α : Type u_2} [Preorder α] [LocallyFiniteOrderBot α] {a : α} :
Iio a ⊆ Iic a
source
theorem BddAbove.finite {α : Type u_2} [Preorder α] [LocallyFiniteOrderBot α] {s : Set α} (hs : BddAbove s) :
s.Finite
source
theorem Set.Infinite.not_bddAbove {α : Type u_2} [Preorder α] [LocallyFiniteOrderBot α] {s : Set α} :
s.Infinite → ¬BddAbove s
source
theorem Finset.filter_gt_eq_Iio {α : Type u_2} [Preorder α] [LocallyFiniteOrderBot α] {a : α} [Fintype α] [DecidablePred fun (x : α) => x < a] :
{x : α | x < a} = Iio a
source
theorem Finset.filter_ge_eq_Iic {α : Type u_2} [Preorder α] [LocallyFiniteOrderBot α] {a : α} [Fintype α] [DecidablePred fun (x : α) => x ≤ a] :
{x : α | x ≤ a} = Iic a
source
@[simp]
theorem Finset.Icc_bot {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrder α] [OrderBot α] :
Icc ⊥ a = Iic a
source
@[simp]
theorem Finset.Icc_top {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrder α] [OrderTop α] :
Icc a ⊤ = Ici a
source
@[simp]
theorem Finset.Ico_bot {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrder α] [OrderBot α] :
Ico ⊥ a = Iio a
source
@[simp]
theorem Finset.Ioc_top {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrder α] [OrderTop α] :
Ioc a ⊤ = Ioi a
source
theorem Finset.Icc_bot_top {α : Type u_2} [Preorder α] [LocallyFiniteOrder α] [BoundedOrder α] [Fintype α] :
Icc ⊥ ⊤ = univ
source
theorem Finset.disjoint_Ioi_Iio {α : Type u_2} [Preorder α] [LocallyFiniteOrderTop α] [LocallyFiniteOrderBot α] (a : α) :
Disjoint (Ioi a) (Iio a)
source
@[simp]
theorem Finset.Icc_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] (a : α) :
Icc a a = {a}
source
@[simp]
theorem Finset.Icc_eq_singleton_iff {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b c : α} :
Icc a b = {c} ↔ a = c ∧ b = c
source
theorem Finset.Ico_disjoint_Ico_consecutive {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] (a b c : α) :
Disjoint (Ico a b) (Ico b c)
source
@[simp]
theorem Finset.Ici_top {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] [OrderTop α] :
Ici ⊤ = {⊤}
source
@[simp]
theorem Finset.Iic_bot {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] [OrderBot α] :
Iic ⊥ = {⊥}
source
@[simp]
theorem Finset.Icc_erase_left {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] (a b : α) :
(Icc a b).erase a = Ioc a b
source
@[simp]
theorem Finset.Icc_erase_right {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] (a b : α) :
(Icc a b).erase b = Ico a b
source
@[simp]
theorem Finset.Ico_erase_left {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] (a b : α) :
(Ico a b).erase a = Ioo a b
source
@[simp]
theorem Finset.Ioc_erase_right {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] (a b : α) :
(Ioc a b).erase b = Ioo a b
source
@[simp]
theorem Finset.Icc_diff_both {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] (a b : α) :
Icc a b \ {a, b} = Ioo a b
source
@[simp]
theorem Finset.Ico_insert_right {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} [DecidableEq α] (h : a ≤ b) :
insert b (Ico a b) = Icc a b
source
@[simp]
theorem Finset.Ioc_insert_left {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} [DecidableEq α] (h : a ≤ b) :
insert a (Ioc a b) = Icc a b
source
@[simp]
theorem Finset.Ioo_insert_left {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} [DecidableEq α] (h : a < b) :
insert a (Ioo a b) = Ico a b
source
@[simp]
theorem Finset.Ioo_insert_right {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} [DecidableEq α] (h : a < b) :
insert b (Ioo a b) = Ioc a b
source
@[simp]
theorem Finset.Icc_diff_Ico_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} [DecidableEq α] (h : a ≤ b) :
Icc a b \ Ico a b = {b}
source
@[simp]
theorem Finset.Icc_diff_Ioc_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} [DecidableEq α] (h : a ≤ b) :
Icc a b \ Ioc a b = {a}
source
@[simp]
theorem Finset.Icc_diff_Ioo_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} [DecidableEq α] (h : a ≤ b) :
Icc a b \ Ioo a b = {a, b}
source
@[simp]
theorem Finset.Ico_diff_Ioo_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} [DecidableEq α] (h : a < b) :
Ico a b \ Ioo a b = {a}
source
@[simp]
theorem Finset.Ioc_diff_Ioo_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} [DecidableEq α] (h : a < b) :
Ioc a b \ Ioo a b = {b}
source
@[simp]
theorem Finset.Ico_inter_Ico_consecutive {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] (a b c : α) :
Ico a b ∩ Ico b c = ∅
source
theorem Finset.Icc_eq_cons_Ico {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} (h : a ≤ b) :
Icc a b = cons b (Ico a b) ⋯

`Finset.cons` version of `Finset.Ico_insert_right`.

source
theorem Finset.Icc_eq_cons_Ioc {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} (h : a ≤ b) :
Icc a b = cons a (Ioc a b) ⋯

`Finset.cons` version of `Finset.Ioc_insert_left`.

source
theorem Finset.Ioc_eq_cons_Ioo {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} (h : a < b) :
Ioc a b = cons b (Ioo a b) ⋯

`Finset.cons` version of `Finset.Ioo_insert_right`.

source
theorem Finset.Ico_eq_cons_Ioo {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} (h : a < b) :
Ico a b = cons a (Ioo a b) ⋯

`Finset.cons` version of `Finset.Ioo_insert_left`.

source
theorem Finset.Ico_filter_le_left {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} [DecidablePred fun (x : α) => x ≤ a] (hab : a < b) :
{x ∈ Ico a b | x ≤ a} = {a}
source
theorem Finset.card_Ico_eq_card_Icc_sub_one {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] (a b : α) :
(Ico a b).card = (Icc a b).card - 1
source
theorem Finset.card_Ioc_eq_card_Icc_sub_one {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] (a b : α) :
(Ioc a b).card = (Icc a b).card - 1
source
theorem Finset.card_Ioo_eq_card_Ico_sub_one {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] (a b : α) :
(Ioo a b).card = (Ico a b).card - 1
source
theorem Finset.card_Ioo_eq_card_Ioc_sub_one {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] (a b : α) :
(Ioo a b).card = (Ioc a b).card - 1
source
theorem Finset.card_Ioo_eq_card_Icc_sub_two {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] (a b : α) :
(Ioo a b).card = (Icc a b).card - 2
source
theorem Finset.uIcc_map_sectL {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (a b : α) (c : β) :
map (Function.Embedding.sectL α c) (uIcc a b) = uIcc (a, c) (b, c)
source
theorem Finset.Icc_map_sectL {α : Type u_2} {β : Type u_3} [Preorder α] [PartialOrder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (a b : α) (c : β) :
map (Function.Embedding.sectL α c) (Icc a b) = Icc (a, c) (b, c)
source
theorem Finset.Ioc_map_sectL {α : Type u_2} {β : Type u_3} [Preorder α] [PartialOrder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (a b : α) (c : β) :
map (Function.Embedding.sectL α c) (Ioc a b) = Ioc (a, c) (b, c)
source
theorem Finset.Ico_map_sectL {α : Type u_2} {β : Type u_3} [Preorder α] [PartialOrder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (a b : α) (c : β) :
map (Function.Embedding.sectL α c) (Ico a b) = Ico (a, c) (b, c)
source
theorem Finset.Ioo_map_sectL {α : Type u_2} {β : Type u_3} [Preorder α] [PartialOrder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (a b : α) (c : β) :
map (Function.Embedding.sectL α c) (Ioo a b) = Ioo (a, c) (b, c)
source
theorem Finset.uIcc_map_sectR {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (c : α) (a b : β) :
map (Function.Embedding.sectR c β) (uIcc a b) = uIcc (c, a) (c, b)
source
theorem Finset.Icc_map_sectR {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (c : α) (a b : β) :
map (Function.Embedding.sectR c β) (Icc a b) = Icc (c, a) (c, b)
source
theorem Finset.Ioc_map_sectR {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (c : α) (a b : β) :
map (Function.Embedding.sectR c β) (Ioc a b) = Ioc (c, a) (c, b)
source
theorem Finset.Ico_map_sectR {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (c : α) (a b : β) :
map (Function.Embedding.sectR c β) (Ico a b) = Ico (c, a) (c, b)
source
theorem Finset.Ioo_map_sectR {α : Type u_2} {β : Type u_3} [PartialOrder α] [Preorder β] [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableLE (α × β)] (c : α) (a b : β) :
map (Function.Embedding.sectR c β) (Ioo a b) = Ioo (c, a) (c, b)
source
@[simp]
theorem Finset.Ici_erase {α : Type u_2} [PartialOrder α] [LocallyFiniteOrderTop α] [DecidableEq α] (a : α) :
(Ici a).erase a = Ioi a
source
@[simp]
theorem Finset.Ioi_insert {α : Type u_2} [PartialOrder α] [LocallyFiniteOrderTop α] [DecidableEq α] (a : α) :
insert a (Ioi a) = Ici a
source
theorem Finset.notMem_Ioi_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrderTop α] {b : α} :
b ∉ Ioi b
source
@[deprecated Finset.notMem_Ioi_self (since := "2025-05-23")]
theorem Finset.not_mem_Ioi_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrderTop α] {b : α} :
b ∉ Ioi b

Alias of `Finset.notMem_Ioi_self`.

source
theorem Finset.Ici_eq_cons_Ioi {α : Type u_2} [PartialOrder α] [LocallyFiniteOrderTop α] (a : α) :
Ici a = cons a (Ioi a) ⋯

`Finset.cons` version of `Finset.Ioi_insert`.

source
theorem Finset.card_Ioi_eq_card_Ici_sub_one {α : Type u_2} [PartialOrder α] [LocallyFiniteOrderTop α] (a : α) :
(Ioi a).card = (Ici a).card - 1
source
@[simp]
theorem Finset.Iic_erase {α : Type u_2} [PartialOrder α] [LocallyFiniteOrderBot α] [DecidableEq α] (b : α) :
(Iic b).erase b = Iio b
source
@[simp]
theorem Finset.Iio_insert {α : Type u_2} [PartialOrder α] [LocallyFiniteOrderBot α] [DecidableEq α] (b : α) :
insert b (Iio b) = Iic b
source
theorem Finset.notMem_Iio_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrderBot α] {b : α} :
b ∉ Iio b
source
@[deprecated Finset.notMem_Iio_self (since := "2025-05-23")]
theorem Finset.not_mem_Iio_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrderBot α] {b : α} :
b ∉ Iio b

Alias of `Finset.notMem_Iio_self`.

source
theorem Finset.Iic_eq_cons_Iio {α : Type u_2} [PartialOrder α] [LocallyFiniteOrderBot α] (b : α) :
Iic b = cons b (Iio b) ⋯

`Finset.cons` version of `Finset.Iio_insert`.

source
theorem Finset.card_Iio_eq_card_Iic_sub_one {α : Type u_2} [PartialOrder α] [LocallyFiniteOrderBot α] (a : α) :
(Iio a).card = (Iic a).card - 1
source
theorem Finset.sup'_Iic {α : Type u_2} [SemilatticeSup α] [LocallyFiniteOrderBot α] (a : α) :
(Iic a).sup' ⋯ id = a
source
@[simp]
theorem Finset.sup_Iic {α : Type u_2} [SemilatticeSup α] [LocallyFiniteOrderBot α] [OrderBot α] (a : α) :
(Iic a).sup id = a
source
theorem Finset.image_subset_Iic_sup {ι : Type u_1} {α : Type u_2} [SemilatticeSup α] [LocallyFiniteOrderBot α] [OrderBot α] [DecidableEq α] (f : ι → α) (s : Finset ι) :
image f s ⊆ Iic (s.sup f)
source
theorem Finset.subset_Iic_sup_id {α : Type u_2} [SemilatticeSup α] [LocallyFiniteOrderBot α] [OrderBot α] (s : Finset α) :
s ⊆ Iic (s.sup id)
source
theorem Finset.inf'_Ici {α : Type u_2} [SemilatticeInf α] [LocallyFiniteOrderTop α] (a : α) :
(Ici a).inf' ⋯ id = a
source
@[simp]
theorem Finset.inf_Ici {α : Type u_2} [SemilatticeInf α] [LocallyFiniteOrderTop α] [OrderTop α] (a : α) :
(Ici a).inf id = a
source
theorem Finset.Ico_subset_Ico_iff {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a₁ b₁ a₂ b₂ : α} (h : a₁ < b₁) :
Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
source
theorem Finset.Ico_union_Ico_eq_Ico {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) :
Ico a b ∪ Ico b c = Ico a c
source
@[simp]
theorem Finset.Ioc_union_Ioc_eq_Ioc {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b c : α} (h₁ : a ≤ b) (h₂ : b ≤ c) :
Ioc a b ∪ Ioc b c = Ioc a c
source
theorem Finset.Ico_subset_Ico_union_Ico {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b c : α} :
Ico a c ⊆ Ico a b ∪ Ico b c
source
theorem Finset.Ico_union_Ico' {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b c d : α} (hcb : c ≤ b) (had : a ≤ d) :
Ico a b ∪ Ico c d = Ico (min a c) (max b d)
source
theorem Finset.Ico_union_Ico {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b c d : α} (h₁ : min a b ≤ max c d) (h₂ : min c d ≤ max a b) :
Ico a b ∪ Ico c d = Ico (min a c) (max b d)
source
theorem Finset.Ico_inter_Ico {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b c d : α} :
Ico a b ∩ Ico c d = Ico (max a c) (min b d)
source
theorem Finset.Ioc_inter_Ioc {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b c d : α} :
Ioc a b ∩ Ioc c d = Ioc (max a c) (min b d)
source
@[simp]
theorem Finset.Ico_filter_lt {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] (a b c : α) :
{x ∈ Ico a b | x < c} = Ico a (min b c)
source
@[simp]
theorem Finset.Ico_filter_le {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] (a b c : α) :
{x ∈ Ico a b | c ≤ x} = Ico (max a c) b
source
@[simp]
theorem Finset.Ioo_filter_lt {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] (a b c : α) :
{x ∈ Ioo a b | x < c} = Ioo a (min b c)
source
@[simp]
theorem Finset.Iio_filter_lt {α : Type u_3} [LinearOrder α] [LocallyFiniteOrderBot α] (a b : α) :
{x ∈ Iio a | x < b} = Iio (min a b)
source
@[simp]
theorem Finset.Ico_diff_Ico_left {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] (a b c : α) :
Ico a b \ Ico a c = Ico (max a c) b
source
@[simp]
theorem Finset.Ico_diff_Ico_right {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] (a b c : α) :
Ico a b \ Ico c b = Ico a (min b c)
source
@[simp]
theorem Finset.Ioc_disjoint_Ioc {α : Type u_2} {a₁ a₂ b₁ b₂ : α} [LinearOrder α] [LocallyFiniteOrder α] :
Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
source
theorem Finset.Iic_diff_Ioc {α : Type u_2} {a b : α} [LinearOrder α] [LocallyFiniteOrder α] [LocallyFiniteOrderBot α] :
Iic b \ Ioc a b = Iic (min a b)
source
theorem Finset.Iic_diff_Ioc_self_of_le {α : Type u_2} {a b : α} [LinearOrder α] [LocallyFiniteOrder α] [LocallyFiniteOrderBot α] (hab : a ≤ b) :
Iic b \ Ioc a b = Iic a
source
theorem Finset.Iic_union_Ioc_eq_Iic {α : Type u_2} {a b : α} [LinearOrder α] [LocallyFiniteOrder α] [LocallyFiniteOrderBot α] (h : a ≤ b) :
Iic a ∪ Ioc a b = Iic b
source
theorem Set.Infinite.exists_gt {α : Type u_2} [LinearOrder α] [LocallyFiniteOrderBot α] {s : Set α} (hs : s.Infinite) (a : α) :
∃ b ∈ s, a < b
source
theorem Set.infinite_iff_exists_gt {α : Type u_2} [LinearOrder α] [LocallyFiniteOrderBot α] {s : Set α} [Nonempty α] :
s.Infinite ↔ ∀ (a : α), ∃ b ∈ s, a < b
source
theorem Set.Infinite.exists_lt {α : Type u_2} [LinearOrder α] [LocallyFiniteOrderTop α] {s : Set α} (hs : s.Infinite) (a : α) :
∃ b ∈ s, b < a
source
theorem Set.infinite_iff_exists_lt {α : Type u_2} [LinearOrder α] [LocallyFiniteOrderTop α] {s : Set α} [Nonempty α] :
s.Infinite ↔ ∀ (a : α), ∃ b ∈ s, b < a
source
theorem Finset.Ioi_disjUnion_Iio {α : Type u_2} [LinearOrder α] [Fintype α] [LocallyFiniteOrderTop α] [LocallyFiniteOrderBot α] (a : α) :
(Ioi a).disjUnion (Iio a) ⋯ = {a}ᶜ
source
theorem Finset.uIcc_toDual {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] (a b : α) :
uIcc (OrderDual.toDual a) (OrderDual.toDual b) = map OrderDual.toDual.toEmbedding (uIcc a b)
source
@[simp]
theorem Finset.uIcc_of_le {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a b : α} (h : a ≤ b) :
uIcc a b = Icc a b
source
@[simp]
theorem Finset.uIcc_of_ge {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a b : α} (h : b ≤ a) :
uIcc a b = Icc b a
source
theorem Finset.uIcc_comm {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] (a b : α) :
uIcc a b = uIcc b a
source
theorem Finset.uIcc_self {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a : α} :
uIcc a a = {a}
source
@[simp]
theorem Finset.nonempty_uIcc {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a b : α} :
(uIcc a b).Nonempty
source
theorem Finset.Icc_subset_uIcc {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a b : α} :
Icc a b ⊆ uIcc a b
source
theorem Finset.Icc_subset_uIcc' {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a b : α} :
Icc b a ⊆ uIcc a b
source
theorem Finset.left_mem_uIcc {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a b : α} :
a ∈ uIcc a b
source
theorem Finset.right_mem_uIcc {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a b : α} :
b ∈ uIcc a b
source
theorem Finset.mem_uIcc_of_le {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a b x : α} (ha : a ≤ x) (hb : x ≤ b) :
x ∈ uIcc a b
source
theorem Finset.mem_uIcc_of_ge {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a b x : α} (hb : b ≤ x) (ha : x ≤ a) :
x ∈ uIcc a b
source
theorem Finset.uIcc_subset_uIcc {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a₁ a₂ b₁ b₂ : α} (h₁ : a₁ ∈ uIcc a₂ b₂) (h₂ : b₁ ∈ uIcc a₂ b₂) :
uIcc a₁ b₁ ⊆ uIcc a₂ b₂
source
theorem Finset.uIcc_subset_Icc {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ ∈ Icc a₂ b₂) (hb : b₁ ∈ Icc a₂ b₂) :
uIcc a₁ b₁ ⊆ Icc a₂ b₂
source
theorem Finset.uIcc_subset_uIcc_iff_mem {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a₁ a₂ b₁ b₂ : α} :
uIcc a₁ b₁ ⊆ uIcc a₂ b₂ ↔ a₁ ∈ uIcc a₂ b₂ ∧ b₁ ∈ uIcc a₂ b₂
source
theorem Finset.uIcc_subset_uIcc_iff_le' {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a₁ a₂ b₁ b₂ : α} :
uIcc a₁ b₁ ⊆ uIcc a₂ b₂ ↔ a₂ ⊓ b₂ ≤ a₁ ⊓ b₁ ∧ a₁ ⊔ b₁ ≤ a₂ ⊔ b₂
source
theorem Finset.uIcc_subset_uIcc_right {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a b x : α} (h : x ∈ uIcc a b) :
uIcc x b ⊆ uIcc a b
source
theorem Finset.uIcc_subset_uIcc_left {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a b x : α} (h : x ∈ uIcc a b) :
uIcc a x ⊆ uIcc a b
source
theorem Finset.eq_of_mem_uIcc_of_mem_uIcc {α : Type u_2} [DistribLattice α] [LocallyFiniteOrder α] {a b c : α} :
a ∈ uIcc b c → b ∈ uIcc a c → a = b
source
theorem Finset.eq_of_mem_uIcc_of_mem_uIcc' {α : Type u_2} [DistribLattice α] [LocallyFiniteOrder α] {a b c : α} :
b ∈ uIcc a c → c ∈ uIcc a b → b = c
source
theorem Finset.uIcc_injective_right {α : Type u_2} [DistribLattice α] [LocallyFiniteOrder α] (a : α) :
Function.Injective fun (b : α) => uIcc b a
source
theorem Finset.uIcc_injective_left {α : Type u_2} [DistribLattice α] [LocallyFiniteOrder α] (a : α) :
Function.Injective (uIcc a)
source
theorem Finset.Icc_min_max {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b : α} :
Icc (min a b) (max a b) = uIcc a b
source
theorem Finset.uIcc_of_not_le {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b : α} (h : ¬a ≤ b) :
uIcc a b = Icc b a
source
theorem Finset.uIcc_of_not_ge {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b : α} (h : ¬b ≤ a) :
uIcc a b = Icc a b
source
theorem Finset.uIcc_eq_union {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b : α} :
uIcc a b = Icc a b ∪ Icc b a
source
theorem Finset.mem_uIcc' {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b c : α} :
a ∈ uIcc b c ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b
source
theorem Finset.notMem_uIcc_of_lt {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b c : α} :
c < a → c < b → c ∉ uIcc a b
source
@[deprecated Finset.notMem_uIcc_of_lt (since := "2025-05-23")]
theorem Finset.not_mem_uIcc_of_lt {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b c : α} :
c < a → c < b → c ∉ uIcc a b

Alias of `Finset.notMem_uIcc_of_lt`.

source
theorem Finset.notMem_uIcc_of_gt {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b c : α} :
a < c → b < c → c ∉ uIcc a b
source
@[deprecated Finset.notMem_uIcc_of_gt (since := "2025-05-23")]
theorem Finset.not_mem_uIcc_of_gt {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b c : α} :
a < c → b < c → c ∉ uIcc a b

Alias of `Finset.notMem_uIcc_of_gt`.

source
theorem Finset.uIcc_subset_uIcc_iff_le {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a₁ a₂ b₁ b₂ : α} :
uIcc a₁ b₁ ⊆ uIcc a₂ b₂ ↔ min a₂ b₂ ≤ min a₁ b₁ ∧ max a₁ b₁ ≤ max a₂ b₂
source
theorem Finset.uIcc_subset_uIcc_union_uIcc {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b c : α} :
uIcc a c ⊆ uIcc a b ∪ uIcc b c

A sort of triangle inequality.

### `⩿`, `⋖` and monotonicity #

source
@[irreducible]
theorem transGen_wcovBy_of_le {α : Type u_2} [Preorder α] [LocallyFiniteOrder α] {x y : α} (hxy : x ≤ y) :
Relation.TransGen (fun (x1 x2 : α) => x1 ⩿ x2) x y
source
theorem le_iff_transGen_wcovBy {α : Type u_2} [Preorder α] [LocallyFiniteOrder α] {x y : α} :
x ≤ y ↔ Relation.TransGen (fun (x1 x2 : α) => x1 ⩿ x2) x y

In a locally finite preorder, `≤` is the transitive closure of `⩿`.

source
theorem le_iff_reflTransGen_covBy {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {x y : α} :
x ≤ y ↔ Relation.ReflTransGen (fun (x1 x2 : α) => x1 ⋖ x2) x y

In a locally finite partial order, `≤` is the reflexive transitive closure of `⋖`.

source
@[irreducible]
theorem transGen_covBy_of_lt {α : Type u_2} [Preorder α] [LocallyFiniteOrder α] {x y : α} (hxy : x < y) :
Relation.TransGen (fun (x1 x2 : α) => x1 ⋖ x2) x y
source
theorem lt_iff_transGen_covBy {α : Type u_2} [Preorder α] [LocallyFiniteOrder α] {x y : α} :
x < y ↔ Relation.TransGen (fun (x1 x2 : α) => x1 ⋖ x2) x y

In a locally finite preorder, `<` is the transitive closure of `⋖`.

source
theorem monotone_iff_forall_wcovBy {α : Type u_2} {β : Type u_3} [Preorder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) :
Monotone f ↔ ∀ (a b : α), a ⩿ b → f a ≤ f b

A function from a locally finite preorder is monotone if and only if it is monotone when restricted to pairs satisfying `a ⩿ b`.

source
theorem monotone_iff_forall_covBy {α : Type u_2} {β : Type u_3} [PartialOrder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) :
Monotone f ↔ ∀ (a b : α), a ⋖ b → f a ≤ f b

A function from a locally finite partial order is monotone if and only if it is monotone when restricted to pairs satisfying `a ⋖ b`.

source
theorem strictMono_iff_forall_covBy {α : Type u_2} {β : Type u_3} [Preorder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) :
StrictMono f ↔ ∀ (a b : α), a ⋖ b → f a < f b

A function from a locally finite preorder is strictly monotone if and only if it is strictly monotone when restricted to pairs satisfying `a ⋖ b`.

source
theorem antitone_iff_forall_wcovBy {α : Type u_2} {β : Type u_3} [Preorder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) :
Antitone f ↔ ∀ (a b : α), a ⩿ b → f b ≤ f a

A function from a locally finite preorder is antitone if and only if it is antitone when restricted to pairs satisfying `a ⩿ b`.

source
theorem antitone_iff_forall_covBy {α : Type u_2} {β : Type u_3} [PartialOrder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) :
Antitone f ↔ ∀ (a b : α), a ⋖ b → f b ≤ f a

A function from a locally finite partial order is antitone if and only if it is antitone when restricted to pairs satisfying `a ⋖ b`.

source
theorem strictAnti_iff_forall_covBy {α : Type u_2} {β : Type u_3} [Preorder α] [LocallyFiniteOrder α] [Preorder β] (f : α → β) :
StrictAnti f ↔ ∀ (a b : α), a ⋖ b → f b < f a

A function from a locally finite preorder is strictly antitone if and only if it is strictly antitone when restricted to pairs satisfying `a ⋖ b`.