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.

@[simp]

theorem Finset.nonempty_Icc {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] : (Icc a b).Nonempty ↔ a ≤ b

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.

@[simp]

theorem Finset.nonempty_Ico {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] : (Ico a b).Nonempty ↔ a < b

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.

@[simp]

theorem Finset.nonempty_Ioc {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] : (Ioc a b).Nonempty ↔ a < b

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.

@[simp]

theorem Finset.nonempty_Ioo {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] [DenselyOrdered α] : (Ioo a b).Nonempty ↔ a < b

@[simp]

theorem Finset.Icc_eq_empty_iff {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] : Icc a b = ∅ ↔ ¬a ≤ b

@[simp]

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

@[simp]

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

@[simp]

theorem Finset.Ioo_eq_empty_iff {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] [DenselyOrdered α] : Ioo a b = ∅ ↔ ¬a < b

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.

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.

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.

@[simp]

theorem Finset.Ioo_eq_empty {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] (h : ¬a < b) : Ioo a b = ∅

@[simp]

theorem Finset.Icc_eq_empty_of_lt {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] (h : b < a) : Icc a b = ∅

@[simp]

theorem Finset.Ico_eq_empty_of_le {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] (h : b ≤ a) : Ico a b = ∅

@[simp]

theorem Finset.Ioc_eq_empty_of_le {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] (h : b ≤ a) : Ioc a b = ∅

@[simp]

theorem Finset.Ioo_eq_empty_of_le {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] (h : b ≤ a) : Ioo a b = ∅

theorem Finset.left_mem_Icc {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] : a ∈ Icc a b ↔ a ≤ b

theorem Finset.left_mem_Ico {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] : a ∈ Ico a b ↔ a < b

theorem Finset.right_mem_Icc {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] : b ∈ Icc a b ↔ a ≤ b

theorem Finset.right_mem_Ioc {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] : b ∈ Ioc a b ↔ a < b

theorem Finset.left_notMem_Ioc {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] : a ∉ Ioc a b

theorem Finset.left_notMem_Ioo {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] : a ∉ Ioo a b

theorem Finset.right_notMem_Ico {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] : b ∉ Ico a b

theorem Finset.right_notMem_Ioo {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] : b ∉ Ioo a b

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₂

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₂

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₂

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₂

theorem Finset.Icc_subset_Icc_left {α : Type u_2} {a₁ a₂ b : α} [Preorder α] [LocallyFiniteOrder α] (h : a₁ ≤ a₂) : Icc a₂ b ⊆ Icc a₁ b

theorem Finset.Ico_subset_Ico_left {α : Type u_2} {a₁ a₂ b : α} [Preorder α] [LocallyFiniteOrder α] (h : a₁ ≤ a₂) : Ico a₂ b ⊆ Ico a₁ b

theorem Finset.Ioc_subset_Ioc_left {α : Type u_2} {a₁ a₂ b : α} [Preorder α] [LocallyFiniteOrder α] (h : a₁ ≤ a₂) : Ioc a₂ b ⊆ Ioc a₁ b

theorem Finset.Ioo_subset_Ioo_left {α : Type u_2} {a₁ a₂ b : α} [Preorder α] [LocallyFiniteOrder α] (h : a₁ ≤ a₂) : Ioo a₂ b ⊆ Ioo a₁ b

theorem Finset.Icc_subset_Icc_right {α : Type u_2} {a b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (h : b₁ ≤ b₂) : Icc a b₁ ⊆ Icc a b₂

theorem Finset.Ico_subset_Ico_right {α : Type u_2} {a b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (h : b₁ ≤ b₂) : Ico a b₁ ⊆ Ico a b₂

theorem Finset.Ioc_subset_Ioc_right {α : Type u_2} {a b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (h : b₁ ≤ b₂) : Ioc a b₁ ⊆ Ioc a b₂

theorem Finset.Ioo_subset_Ioo_right {α : Type u_2} {a b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (h : b₁ ≤ b₂) : Ioo a b₁ ⊆ Ioo a b₂

theorem Finset.Ico_subset_Ioo_left {α : Type u_2} {a₁ a₂ b : α} [Preorder α] [LocallyFiniteOrder α] (h : a₁ < a₂) : Ico a₂ b ⊆ Ioo a₁ b

theorem Finset.Ioc_subset_Ioo_right {α : Type u_2} {a b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (h : b₁ < b₂) : Ioc a b₁ ⊆ Ioo a b₂

theorem Finset.Icc_subset_Ico_right {α : Type u_2} {a b₁ b₂ : α} [Preorder α] [LocallyFiniteOrder α] (h : b₁ < b₂) : Icc a b₁ ⊆ Ico a b₂

theorem Finset.Ioo_subset_Ico_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] : Ioo a b ⊆ Ico a b

theorem Finset.Ioo_subset_Ioc_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] : Ioo a b ⊆ Ioc a b

theorem Finset.Ico_subset_Icc_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] : Ico a b ⊆ Icc a b

theorem Finset.Ioc_subset_Icc_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] : Ioc a b ⊆ Icc a b

theorem Finset.Ioo_subset_Icc_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrder α] : Ioo a b ⊆ Icc a b

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₂

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₂

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₂

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₂

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₂

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₂

@[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)

theorem not_lt_of_denselyOrdered_of_locallyFinite {α : Type u_2} [Preorder α] [LocallyFiniteOrder α] [DenselyOrdered α] (a b : α) : ¬a < b

theorem Finset.Ico_self {α : Type u_2} (a : α) [Preorder α] [LocallyFiniteOrder α] : Ico a a = ∅

theorem Finset.Ioc_self {α : Type u_2} (a : α) [Preorder α] [LocallyFiniteOrder α] : Ioc a a = ∅

theorem Finset.Ioo_self {α : Type u_2} (a : α) [Preorder α] [LocallyFiniteOrder α] : Ioo a a = ∅

@[implicit_reducible]

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 ⋯

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} = ∅

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

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

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

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} = ∅

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

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

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

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

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

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

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

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

@[simp]

theorem Finset.Ioi_eq_empty {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderTop α] : Ioi a = ∅ ↔ IsMax a

@[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.

@[simp]

theorem Finset.Ioi_nonempty {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderTop α] : (Ioi a).Nonempty ↔ ¬IsMax a

theorem Finset.Ioi_top {α : Type u_2} [Preorder α] [LocallyFiniteOrderTop α] [OrderTop α] : Ioi ⊤ = ∅

@[simp]

theorem Finset.Ici_bot {α : Type u_2} [Preorder α] [LocallyFiniteOrderTop α] [OrderBot α] [Fintype α] : Ici ⊥ = univ

@[simp]

theorem Finset.nonempty_Ici {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderTop α] : (Ici a).Nonempty

theorem Finset.nonempty_Ioi {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderTop α] : (Ioi a).Nonempty ↔ ¬IsMax a

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.

@[simp]

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

@[simp]

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

theorem Finset.Ioi_subset_Ioi {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderTop α] (h : a ≤ b) : Ioi b ⊆ Ioi a

theorem Finset.Ioi_ssubset_Ioi {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderTop α] (h : a < b) : Ioi b ⊂ Ioi a

theorem Finset.Icc_subset_Ici_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderTop α] [LocallyFiniteOrder α] : Icc a b ⊆ Ici a

theorem Finset.Ico_subset_Ici_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderTop α] [LocallyFiniteOrder α] : Ico a b ⊆ Ici a

theorem Finset.Ioc_subset_Ioi_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderTop α] [LocallyFiniteOrder α] : Ioc a b ⊆ Ioi a

theorem Finset.Ioo_subset_Ioi_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderTop α] [LocallyFiniteOrder α] : Ioo a b ⊆ Ioi a

theorem Finset.Ioc_subset_Ici_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderTop α] [LocallyFiniteOrder α] : Ioc a b ⊆ Ici a

theorem Finset.Ioo_subset_Ici_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderTop α] [LocallyFiniteOrder α] : Ioo a b ⊆ Ici a

@[simp]

theorem Finset.Iio_eq_empty {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderBot α] : Iio a = ∅ ↔ IsMin a

@[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.

@[simp]

theorem Finset.Iio_nonempty {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderBot α] : (Iio a).Nonempty ↔ ¬IsMin a

theorem Finset.Iio_bot {α : Type u_2} [Preorder α] [LocallyFiniteOrderBot α] [OrderBot α] : Iio ⊥ = ∅

@[simp]

theorem Finset.Iic_top {α : Type u_2} [Preorder α] [LocallyFiniteOrderBot α] [OrderTop α] [Fintype α] : Iic ⊤ = univ

@[simp]

theorem Finset.nonempty_Iic {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderBot α] : (Iic a).Nonempty

theorem Finset.nonempty_Iio {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderBot α] : (Iio a).Nonempty ↔ ¬IsMin a

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.

@[simp]

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

@[simp]

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

theorem Finset.Iio_subset_Iio {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderBot α] (h : a ≤ b) : Iio a ⊆ Iio b

theorem Finset.Iio_ssubset_Iio {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderBot α] (h : a < b) : Iio a ⊂ Iio b

theorem Finset.sup_Iic_of_monotone {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrderBot α] {β : Type u_3} [SemilatticeSup β] [OrderBot β] {f : α → β} (hf : Monotone f) : (Iic a).sup f = f a

theorem Finset.Icc_subset_Iic_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderBot α] [LocallyFiniteOrder α] : Icc a b ⊆ Iic b

theorem Finset.Ioc_subset_Iic_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderBot α] [LocallyFiniteOrder α] : Ioc a b ⊆ Iic b

theorem Finset.Ico_subset_Iio_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderBot α] [LocallyFiniteOrder α] : Ico a b ⊆ Iio b

theorem Finset.Ioo_subset_Iio_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderBot α] [LocallyFiniteOrder α] : Ioo a b ⊆ Iio b

theorem Finset.Ico_subset_Iic_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderBot α] [LocallyFiniteOrder α] : Ico a b ⊆ Iic b

theorem Finset.Ioo_subset_Iic_self {α : Type u_2} {a b : α} [Preorder α] [LocallyFiniteOrderBot α] [LocallyFiniteOrder α] : Ioo a b ⊆ Iic b

theorem Finset.Iic_disjoint_Ioc {α : Type u_2} {a b c : α} [Preorder α] [LocallyFiniteOrderBot α] [LocallyFiniteOrder α] (h : a ≤ b) : Disjoint (Iic a) (Ioc b c)

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 := ⋯ }

theorem Finset.Ioi_subset_Ici_self {α : Type u_2} [Preorder α] [LocallyFiniteOrderTop α] {a : α} : Ioi a ⊆ Ici a

theorem BddBelow.finite {α : Type u_2} [Preorder α] [LocallyFiniteOrderTop α] {s : Set α} (hs : BddBelow s) : s.Finite

theorem Set.Infinite.not_bddBelow {α : Type u_2} [Preorder α] [LocallyFiniteOrderTop α] {s : Set α} : s.Infinite → ¬BddBelow s

theorem Finset.filter_lt_eq_Ioi {α : Type u_2} [Preorder α] [LocallyFiniteOrderTop α] {a : α} [Fintype α] [DecidablePred fun (x : α) => a < x] : {x : α | a < x} = Ioi a

theorem Finset.filter_le_eq_Ici {α : Type u_2} [Preorder α] [LocallyFiniteOrderTop α] {a : α} [Fintype α] [DecidablePred fun (x : α) => a ≤ x] : {x : α | a ≤ x} = Ici a

theorem Finset.Iio_subset_Iic_self {α : Type u_2} [Preorder α] [LocallyFiniteOrderBot α] {a : α} : Iio a ⊆ Iic a

theorem BddAbove.finite {α : Type u_2} [Preorder α] [LocallyFiniteOrderBot α] {s : Set α} (hs : BddAbove s) : s.Finite

theorem Set.Infinite.not_bddAbove {α : Type u_2} [Preorder α] [LocallyFiniteOrderBot α] {s : Set α} : s.Infinite → ¬BddAbove s

theorem Finset.filter_gt_eq_Iio {α : Type u_2} [Preorder α] [LocallyFiniteOrderBot α] {a : α} [Fintype α] [DecidablePred fun (x : α) => x < a] : {x : α | x < a} = Iio a

theorem Finset.filter_ge_eq_Iic {α : Type u_2} [Preorder α] [LocallyFiniteOrderBot α] {a : α} [Fintype α] [DecidablePred fun (x : α) => x ≤ a] : {x : α | x ≤ a} = Iic a

@[simp]

theorem Finset.Icc_bot {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrder α] [OrderBot α] : Icc ⊥ a = Iic a

@[simp]

theorem Finset.Icc_top {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrder α] [OrderTop α] : Icc a ⊤ = Ici a

@[simp]

theorem Finset.Ico_bot {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrder α] [OrderBot α] : Ico ⊥ a = Iio a

@[simp]

theorem Finset.Ioc_top {α : Type u_2} {a : α} [Preorder α] [LocallyFiniteOrder α] [OrderTop α] : Ioc a ⊤ = Ioi a

theorem Finset.Icc_bot_top {α : Type u_2} [Preorder α] [LocallyFiniteOrder α] [BoundedOrder α] [Fintype α] : Icc ⊥ ⊤ = univ

theorem Finset.disjoint_Ioi_Iio {α : Type u_2} [Preorder α] [LocallyFiniteOrderTop α] [LocallyFiniteOrderBot α] (a : α) : Disjoint (Ioi a) (Iio a)

@[simp]

theorem Finset.Icc_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] (a : α) : Icc a a = {a}

@[simp]

theorem Finset.Icc_eq_singleton_iff {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b c : α} : Icc a b = {c} ↔ a = c ∧ b = c

theorem Finset.Ico_disjoint_Ico_consecutive {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] (a b c : α) : Disjoint (Ico a b) (Ico b c)

@[simp]

theorem Finset.Ici_top {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] [OrderTop α] : Ici ⊤ = {⊤}

@[simp]

theorem Finset.Iic_bot {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] [OrderBot α] : Iic ⊥ = {⊥}

@[implicit_reducible]

instance Finset.instUniqueSubtypeMemIicBot {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] [OrderBot α] : Unique ↥(Iic ⊥)

Equations

• Finset.instUniqueSubtypeMemIicBot = ⋯.mpr inferInstance

@[simp]

theorem Finset.Icc_erase_left {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] (a b : α) : (Icc a b).erase a = Ioc a b

@[simp]

theorem Finset.Icc_erase_right {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] (a b : α) : (Icc a b).erase b = Ico a b

@[simp]

theorem Finset.Ico_erase_left {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] (a b : α) : (Ico a b).erase a = Ioo a b

@[simp]

theorem Finset.Ioc_erase_right {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] (a b : α) : (Ioc a b).erase b = Ioo a b

@[simp]

theorem Finset.Icc_sdiff_both {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] (a b : α) : Icc a b \ {a, b} = Ioo a b

@[deprecated Finset.Icc_sdiff_both (since := "2026-06-03")]

theorem Finset.Icc_diff_both {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] (a b : α) : Icc a b \ {a, b} = Ioo a b

Alias of Finset.Icc_sdiff_both.

@[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

@[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

@[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

@[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

@[simp]

theorem Finset.Icc_sdiff_Ico_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} [DecidableEq α] (h : a ≤ b) : Icc a b \ Ico a b = {b}

@[deprecated Finset.Icc_sdiff_Ico_self (since := "2026-06-03")]

theorem Finset.Icc_diff_Ico_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} [DecidableEq α] (h : a ≤ b) : Icc a b \ Ico a b = {b}

Alias of Finset.Icc_sdiff_Ico_self.

@[simp]

theorem Finset.Icc_sdiff_Ioc_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} [DecidableEq α] (h : a ≤ b) : Icc a b \ Ioc a b = {a}

@[deprecated Finset.Icc_sdiff_Ioc_self (since := "2026-06-03")]

theorem Finset.Icc_diff_Ioc_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} [DecidableEq α] (h : a ≤ b) : Icc a b \ Ioc a b = {a}

Alias of Finset.Icc_sdiff_Ioc_self.

@[simp]

theorem Finset.Icc_sdiff_Ioo_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} [DecidableEq α] (h : a ≤ b) : Icc a b \ Ioo a b = {a, b}

@[deprecated Finset.Icc_sdiff_Ioo_self (since := "2026-06-03")]

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}

Alias of Finset.Icc_sdiff_Ioo_self.

@[simp]

theorem Finset.Ico_sdiff_Ioo_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} [DecidableEq α] (h : a < b) : Ico a b \ Ioo a b = {a}

@[deprecated Finset.Ico_sdiff_Ioo_self (since := "2026-06-03")]

theorem Finset.Ico_diff_Ioo_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} [DecidableEq α] (h : a < b) : Ico a b \ Ioo a b = {a}

Alias of Finset.Ico_sdiff_Ioo_self.

@[simp]

theorem Finset.Ioc_sdiff_Ioo_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} [DecidableEq α] (h : a < b) : Ioc a b \ Ioo a b = {b}

@[deprecated Finset.Ioc_sdiff_Ioo_self (since := "2026-06-03")]

theorem Finset.Ioc_diff_Ioo_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] {a b : α} [DecidableEq α] (h : a < b) : Ioc a b \ Ioo a b = {b}

Alias of Finset.Ioc_sdiff_Ioo_self.

@[simp]

theorem Finset.Ico_inter_Ico_consecutive {α : Type u_2} [PartialOrder α] [LocallyFiniteOrder α] [DecidableEq α] (a b c : α) : Ico a b ∩ Ico b c = ∅

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.

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.

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.

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.

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}

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

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

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

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

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

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

@[simp]

theorem Finset.Ici_erase {α : Type u_2} [PartialOrder α] [LocallyFiniteOrderTop α] [DecidableEq α] (a : α) : (Ici a).erase a = Ioi a

@[simp]

theorem Finset.Ioi_insert {α : Type u_2} [PartialOrder α] [LocallyFiniteOrderTop α] [DecidableEq α] (a : α) : insert a (Ioi a) = Ici a

theorem Finset.notMem_Ioi_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrderTop α] {b : α} : b ∉ Ioi b

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.

theorem Finset.card_Ioi_eq_card_Ici_sub_one {α : Type u_2} [PartialOrder α] [LocallyFiniteOrderTop α] (a : α) : (Ioi a).card = (Ici a).card - 1

@[simp]

theorem Finset.Iic_erase {α : Type u_2} [PartialOrder α] [LocallyFiniteOrderBot α] [DecidableEq α] (b : α) : (Iic b).erase b = Iio b

@[simp]

theorem Finset.Iio_insert {α : Type u_2} [PartialOrder α] [LocallyFiniteOrderBot α] [DecidableEq α] (b : α) : insert b (Iio b) = Iic b

theorem Finset.notMem_Iio_self {α : Type u_2} [PartialOrder α] [LocallyFiniteOrderBot α] {b : α} : b ∉ Iio b

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.

theorem Finset.card_Iio_eq_card_Iic_sub_one {α : Type u_2} [PartialOrder α] [LocallyFiniteOrderBot α] (a : α) : (Iio a).card = (Iic a).card - 1

theorem Finset.sup'_Iic {α : Type u_2} [SemilatticeSup α] [LocallyFiniteOrderBot α] (a : α) : (Iic a).sup' ⋯ id = a

@[simp]

theorem Finset.sup_Iic {α : Type u_2} [SemilatticeSup α] [LocallyFiniteOrderBot α] [OrderBot α] (a : α) : (Iic a).sup id = a

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)

theorem Finset.subset_Iic_sup_id {α : Type u_2} [SemilatticeSup α] [LocallyFiniteOrderBot α] [OrderBot α] (s : Finset α) : s ⊆ Iic (s.sup id)

theorem Finset.inf'_Ici {α : Type u_2} [SemilatticeInf α] [LocallyFiniteOrderTop α] (a : α) : (Ici a).inf' ⋯ id = a

@[simp]

theorem Finset.inf_Ici {α : Type u_2} [SemilatticeInf α] [LocallyFiniteOrderTop α] [OrderTop α] (a : α) : (Ici a).inf id = a

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₂

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

@[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

theorem Finset.Ico_subset_Ico_union_Ico {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b c : α} : Ico a c ⊆ Ico a b ∪ Ico b c

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)

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)

This is a special case of Ico_union_Ico

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)

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)

@[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)

@[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

@[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)

@[simp]

theorem Finset.Iio_filter_lt {α : Type u_3} [LinearOrder α] [LocallyFiniteOrderBot α] (a b : α) : {x ∈ Iio a | x < b} = Iio (min a b)

@[simp]

theorem Finset.Ico_sdiff_Ico_left {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] (a b c : α) : Ico a b \ Ico a c = Ico (max a c) b

@[deprecated Finset.Ico_sdiff_Ico_left (since := "2026-06-03")]

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

Alias of Finset.Ico_sdiff_Ico_left.

@[simp]

theorem Finset.Ico_sdiff_Ico_right {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] (a b c : α) : Ico a b \ Ico c b = Ico a (min b c)

@[deprecated Finset.Ico_sdiff_Ico_right (since := "2026-06-03")]

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)

Alias of Finset.Ico_sdiff_Ico_right.

@[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₁

theorem Finset.Iic_sdiff_Ioc {α : Type u_2} {a b : α} [LinearOrder α] [LocallyFiniteOrder α] [LocallyFiniteOrderBot α] : Iic b \ Ioc a b = Iic (min a b)

@[deprecated Finset.Iic_sdiff_Ioc (since := "2026-06-03")]

theorem Finset.Iic_diff_Ioc {α : Type u_2} {a b : α} [LinearOrder α] [LocallyFiniteOrder α] [LocallyFiniteOrderBot α] : Iic b \ Ioc a b = Iic (min a b)

Alias of Finset.Iic_sdiff_Ioc.

theorem Finset.Iic_sdiff_Ioc_self_of_le {α : Type u_2} {a b : α} [LinearOrder α] [LocallyFiniteOrder α] [LocallyFiniteOrderBot α] (hab : a ≤ b) : Iic b \ Ioc a b = Iic a

@[deprecated Finset.Iic_sdiff_Ioc_self_of_le (since := "2026-06-03")]

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

Alias of Finset.Iic_sdiff_Ioc_self_of_le.

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

theorem Set.Infinite.exists_gt {α : Type u_2} [LinearOrder α] [LocallyFiniteOrderBot α] {s : Set α} (hs : s.Infinite) (a : α) : ∃ b ∈ s, a < b

theorem Set.infinite_iff_exists_gt {α : Type u_2} [LinearOrder α] [LocallyFiniteOrderBot α] {s : Set α} [Nonempty α] : s.Infinite ↔ ∀ (a : α), ∃ b ∈ s, a < b

theorem Set.Infinite.exists_lt {α : Type u_2} [LinearOrder α] [LocallyFiniteOrderTop α] {s : Set α} (hs : s.Infinite) (a : α) : ∃ b ∈ s, b < a

theorem Set.infinite_iff_exists_lt {α : Type u_2} [LinearOrder α] [LocallyFiniteOrderTop α] {s : Set α} [Nonempty α] : s.Infinite ↔ ∀ (a : α), ∃ b ∈ s, b < a

theorem Finset.Ioi_disjUnion_Iio {α : Type u_2} [LinearOrder α] [Fintype α] [LocallyFiniteOrderTop α] [LocallyFiniteOrderBot α] (a : α) : (Ioi a).disjUnion (Iio a) ⋯ = {a}ᶜ

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)

@[simp]

theorem Finset.uIcc_of_le {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a b : α} (h : a ≤ b) : uIcc a b = Icc a b

@[simp]

theorem Finset.uIcc_of_ge {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a b : α} (h : b ≤ a) : uIcc a b = Icc b a

theorem Finset.uIcc_comm {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] (a b : α) : uIcc a b = uIcc b a

theorem Finset.uIcc_self {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a : α} : uIcc a a = {a}

@[simp]

theorem Finset.nonempty_uIcc {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a b : α} : (uIcc a b).Nonempty

theorem Finset.Icc_subset_uIcc {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a b : α} : Icc a b ⊆ uIcc a b

theorem Finset.Icc_subset_uIcc' {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a b : α} : Icc b a ⊆ uIcc a b

theorem Finset.left_mem_uIcc {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a b : α} : a ∈ uIcc a b

theorem Finset.right_mem_uIcc {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a b : α} : b ∈ uIcc a b

theorem Finset.mem_uIcc_of_le {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a b x : α} (ha : a ≤ x) (hb : x ≤ b) : x ∈ uIcc a b

theorem Finset.mem_uIcc_of_ge {α : Type u_2} [Lattice α] [LocallyFiniteOrder α] {a b x : α} (hb : b ≤ x) (ha : x ≤ a) : x ∈ uIcc a b

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₂

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₂

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₂

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₂

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

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

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

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

theorem Finset.uIcc_injective_right {α : Type u_2} [DistribLattice α] [LocallyFiniteOrder α] (a : α) : Function.Injective fun (b : α) => uIcc b a

theorem Finset.uIcc_injective_left {α : Type u_2} [DistribLattice α] [LocallyFiniteOrder α] (a : α) : Function.Injective (uIcc a)

theorem Finset.Icc_min_max {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b : α} : Icc (min a b) (max a b) = uIcc a b

theorem Finset.uIcc_of_not_le {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b : α} (h : ¬a ≤ b) : uIcc a b = Icc b a

theorem Finset.uIcc_of_not_ge {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b : α} (h : ¬b ≤ a) : uIcc a b = Icc a b

theorem Finset.uIcc_eq_union {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b : α} : uIcc a b = Icc a b ∪ Icc b a

theorem Finset.mem_uIcc' {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b c : α} : a ∈ uIcc b c ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b

theorem Finset.notMem_uIcc_of_lt {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b c : α} : c < a → c < b → c ∉ uIcc a b

theorem Finset.notMem_uIcc_of_gt {α : Type u_2} [LinearOrder α] [LocallyFiniteOrder α] {a b c : α} : a < c → b < c → c ∉ uIcc a b

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₂

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

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

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 ⩿.

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 ⋖.

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

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 ⋖.

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.

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.

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.

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.

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.

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.