Intervals as finsets

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

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.

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

theorem Finset.Icc_eq_empty {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} : ¬a ≤ b → Finset.Icc a b = ∅

Alias of the reverse direction of Finset.Icc_eq_empty_iff.

ink

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

Alias of the reverse direction of Finset.Ico_eq_empty_iff.

ink

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

Alias of the reverse direction of Finset.Ioc_eq_empty_iff.

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

theorem Finset.left_not_mem_Ioc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} : ¬a ∈ Finset.Ioc a b

ink

theorem Finset.left_not_mem_Ioo {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} : ¬a ∈ Finset.Ioo a b

ink

theorem Finset.right_not_mem_Ico {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} : ¬b ∈ Finset.Ico a b

ink

theorem Finset.right_not_mem_Ioo {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} : ¬b ∈ Finset.Ioo a b

ink

theorem Finset.Icc_subset_Icc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : Finset.Icc a₁ b₁ ⊆ Finset.Icc a₂ b₂

ink

theorem Finset.Ico_subset_Ico {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : Finset.Ico a₁ b₁ ⊆ Finset.Ico a₂ b₂

ink

theorem Finset.Ioc_subset_Ioc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : Finset.Ioc a₁ b₁ ⊆ Finset.Ioc a₂ b₂

ink

theorem Finset.Ioo_subset_Ioo {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) : Finset.Ioo a₁ b₁ ⊆ Finset.Ioo a₂ b₂

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

theorem Finset.Icc_subset_Icc_iff {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (h₁ : a₁ ≤ b₁) : Finset.Icc a₁ b₁ ⊆ Finset.Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

ink

theorem Finset.Icc_subset_Ioo_iff {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (h₁ : a₁ ≤ b₁) : Finset.Icc a₁ b₁ ⊆ Finset.Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂

ink

theorem Finset.Icc_subset_Ico_iff {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (h₁ : a₁ ≤ b₁) : Finset.Icc a₁ b₁ ⊆ Finset.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂

ink

theorem Finset.Icc_subset_Ioc_iff {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (h₁ : a₁ ≤ b₁) : Finset.Icc a₁ b₁ ⊆ Finset.Ioc a₂ b₂ ↔ a₂ < a₁ ∧ b₁ ≤ b₂

ink

theorem Finset.Icc_ssubset_Icc_left {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (hI : a₂ ≤ b₂) (ha : a₂ < a₁) (hb : b₁ ≤ b₂) : Finset.Icc a₁ b₁ ⊂ Finset.Icc a₂ b₂

ink

theorem Finset.Icc_ssubset_Icc_right {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (hI : a₂ ≤ b₂) (ha : a₂ ≤ a₁) (hb : b₁ < b₂) : Finset.Icc a₁ b₁ ⊂ Finset.Icc a₂ b₂

ink

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

ink

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

ink

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

ink

def Set.fintypeOfMemBounds {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {s : Set α} [inst : 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.fintypeSubset (Set.Icc a b) (_ : ∀ (x : α), x ∈ s → a ≤ x ∧ x ≤ b)

ink

theorem BddBelow.finite_of_bddAbove {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {s : Set α} (h₀ : BddBelow s) (h₁ : BddAbove s) : Set.Finite s

ink

theorem Finset.Ico_filter_lt_of_le_left {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} [inst : DecidablePred fun x => x < c] (hca : c ≤ a) : Finset.filter (fun x => x < c) (Finset.Ico a b) = ∅

ink

theorem Finset.Ico_filter_lt_of_right_le {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} [inst : DecidablePred fun x => x < c] (hbc : b ≤ c) : Finset.filter (fun x => x < c) (Finset.Ico a b) = Finset.Ico a b

ink

theorem Finset.Ico_filter_lt_of_le_right {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} [inst : DecidablePred fun x => x < c] (hcb : c ≤ b) : Finset.filter (fun x => x < c) (Finset.Ico a b) = Finset.Ico a c

ink

theorem Finset.Ico_filter_le_of_le_left {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} [inst : DecidablePred ((fun x x_1 => x ≤ x_1) c)] (hca : c ≤ a) : Finset.filter ((fun x x_1 => x ≤ x_1) c) (Finset.Ico a b) = Finset.Ico a b

ink

theorem Finset.Ico_filter_le_of_right_le {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : DecidablePred ((fun x x_1 => x ≤ x_1) b)] : Finset.filter ((fun x x_1 => x ≤ x_1) b) (Finset.Ico a b) = ∅

ink

theorem Finset.Ico_filter_le_of_left_le {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} [inst : DecidablePred ((fun x x_1 => x ≤ x_1) c)] (hac : a ≤ c) : Finset.filter ((fun x x_1 => x ≤ x_1) c) (Finset.Ico a b) = Finset.Ico c b

ink

theorem Finset.Icc_filter_lt_of_lt_right {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} [inst : DecidablePred fun x => x < c] (h : b < c) : Finset.filter (fun x => x < c) (Finset.Icc a b) = Finset.Icc a b

ink

theorem Finset.Ioc_filter_lt_of_lt_right {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} [inst : DecidablePred fun x => x < c] (h : b < c) : Finset.filter (fun x => x < c) (Finset.Ioc a b) = Finset.Ioc a b

ink

theorem Finset.Iic_filter_lt_of_lt_right {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderBot α] {a : α} {c : α} [inst : DecidablePred fun x => x < c] (h : a < c) : Finset.filter (fun x => x < c) (Finset.Iic a) = Finset.Iic a

ink

theorem Finset.filter_lt_lt_eq_Ioo {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) [inst : Fintype α] [inst : DecidablePred fun j => a < j ∧ j < b] : Finset.filter (fun j => a < j ∧ j < b) Finset.univ = Finset.Ioo a b

ink

theorem Finset.filter_lt_le_eq_Ioc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) [inst : Fintype α] [inst : DecidablePred fun j => a < j ∧ j ≤ b] : Finset.filter (fun j => a < j ∧ j ≤ b) Finset.univ = Finset.Ioc a b

ink

theorem Finset.filter_le_lt_eq_Ico {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) [inst : Fintype α] [inst : DecidablePred fun j => a ≤ j ∧ j < b] : Finset.filter (fun j => a ≤ j ∧ j < b) Finset.univ = Finset.Ico a b

ink

theorem Finset.filter_le_le_eq_Icc {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) [inst : Fintype α] [inst : DecidablePred fun j => a ≤ j ∧ j ≤ b] : Finset.filter (fun j => a ≤ j ∧ j ≤ b) Finset.univ = Finset.Icc a b

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

theorem Finset.filter_lt_eq_Ioi {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] {a : α} [inst : Fintype α] [inst : DecidablePred ((fun x x_1 => x < x_1) a)] : Finset.filter ((fun x x_1 => x < x_1) a) Finset.univ = Finset.Ioi a

ink

theorem Finset.filter_le_eq_Ici {α : Type u_1} [inst : Preorder α] [inst : LocallyFiniteOrderTop α] {a : α} [inst : Fintype α] [inst : DecidablePred ((fun x x_1 => x ≤ x_1) a)] : Finset.filter ((fun x x_1 => x ≤ x_1) a) Finset.univ = Finset.Ici a

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

theorem Finset.Ico_insert_right {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : DecidableEq α] (h : a ≤ b) : insert b (Finset.Ico a b) = Finset.Icc a b

ink

@[simp]

theorem Finset.Ioc_insert_left {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : DecidableEq α] (h : a ≤ b) : insert a (Finset.Ioc a b) = Finset.Icc a b

ink

@[simp]

theorem Finset.Ioo_insert_left {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : DecidableEq α] (h : a < b) : insert a (Finset.Ioo a b) = Finset.Ico a b

ink

@[simp]

theorem Finset.Ioo_insert_right {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : DecidableEq α] (h : a < b) : insert b (Finset.Ioo a b) = Finset.Ioc a b

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

theorem Finset.Icc_eq_cons_Ico {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} (h : a ≤ b) : Finset.Icc a b = Finset.cons b (Finset.Ico a b) (_ : ¬b ∈ Finset.Ico a b)

Finset.cons version of Finset.Ico_insert_right.

ink

theorem Finset.Icc_eq_cons_Ioc {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} (h : a ≤ b) : Finset.Icc a b = Finset.cons a (Finset.Ioc a b) (_ : ¬a ∈ Finset.Ioc a b)

Finset.cons version of Finset.Ioc_insert_left.

ink

theorem Finset.Ioc_eq_cons_Ioo {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} (h : a < b) : Finset.Ioc a b = Finset.cons b (Finset.Ioo a b) (_ : ¬b ∈ Finset.Ioo a b)

Finset.cons version of Finset.Ioo_insert_right.

ink

theorem Finset.Ico_eq_cons_Ioo {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} (h : a < b) : Finset.Ico a b = Finset.cons a (Finset.Ioo a b) (_ : ¬a ∈ Finset.Ioo a b)

Finset.cons version of Finset.Ioo_insert_left.

ink

theorem Finset.Ico_filter_le_left {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} [inst : DecidablePred fun x => x ≤ a] (hab : a < b) : Finset.filter (fun x => x ≤ a) (Finset.Ico a b) = {a}

ink

theorem Finset.card_Ico_eq_card_Icc_sub_one {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) : Finset.card (Finset.Ico a b) = Finset.card (Finset.Icc a b) - 1

ink

theorem Finset.card_Ioc_eq_card_Icc_sub_one {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) : Finset.card (Finset.Ioc a b) = Finset.card (Finset.Icc a b) - 1

ink

theorem Finset.card_Ioo_eq_card_Ico_sub_one {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) : Finset.card (Finset.Ioo a b) = Finset.card (Finset.Ico a b) - 1

ink

theorem Finset.card_Ioo_eq_card_Ioc_sub_one {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) : Finset.card (Finset.Ioo a b) = Finset.card (Finset.Ioc a b) - 1

ink

theorem Finset.card_Ioo_eq_card_Icc_sub_two {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) : Finset.card (Finset.Ioo a b) = Finset.card (Finset.Icc a b) - 2

ink

@[simp]

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

ink

@[simp]

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

ink

theorem Finset.not_mem_Ioi_self {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrderTop α] {b : α} : ¬b ∈ Finset.Ioi b

ink

theorem Finset.Ici_eq_cons_Ioi {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrderTop α] (a : α) : Finset.Ici a = Finset.cons a (Finset.Ioi a) (_ : ¬a ∈ Finset.Ioi a)

Finset.cons version of Finset.Ioi_insert.

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

theorem Finset.not_mem_Iio_self {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrderBot α] {b : α} : ¬b ∈ Finset.Iio b

ink

theorem Finset.Iic_eq_cons_Iio {α : Type u_1} [inst : PartialOrder α] [inst : LocallyFiniteOrderBot α] (b : α) : Finset.Iic b = Finset.cons b (Finset.Iio b) (_ : ¬b ∈ Finset.Iio b)

Finset.cons version of Finset.Iio_insert.

ink

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

ink

theorem Finset.Ico_subset_Ico_iff {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a₁ : α} {b₁ : α} {a₂ : α} {b₂ : α} (h : a₁ < b₁) : Finset.Ico a₁ b₁ ⊆ Finset.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂

ink

theorem Finset.Ico_union_Ico_eq_Ico {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} (hab : a ≤ b) (hbc : b ≤ c) : Finset.Ico a b ∪ Finset.Ico b c = Finset.Ico a c

ink

@[simp]

theorem Finset.Ioc_union_Ioc_eq_Ioc {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} (h₁ : a ≤ b) (h₂ : b ≤ c) : Finset.Ioc a b ∪ Finset.Ioc b c = Finset.Ioc a c

ink

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

ink

theorem Finset.Ico_union_Ico' {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} {d : α} (hcb : c ≤ b) (had : a ≤ d) : Finset.Ico a b ∪ Finset.Ico c d = Finset.Ico (min a c) (max b d)

ink

theorem Finset.Ico_union_Ico {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} {d : α} (h₁ : min a b ≤ max c d) (h₂ : min c d ≤ max a b) : Finset.Ico a b ∪ Finset.Ico c d = Finset.Ico (min a c) (max b d)

ink

theorem Finset.Ico_inter_Ico {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} {d : α} : Finset.Ico a b ∩ Finset.Ico c d = Finset.Ico (max a c) (min b d)

ink

@[simp]

theorem Finset.Ico_filter_lt {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) : Finset.filter (fun x => x < c) (Finset.Ico a b) = Finset.Ico a (min b c)

ink

@[simp]

theorem Finset.Ico_filter_le {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) : Finset.filter (fun x => c ≤ x) (Finset.Ico a b) = Finset.Ico (max a c) b

ink

@[simp]

theorem Finset.Ioo_filter_lt {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) : Finset.filter (fun x => x < c) (Finset.Ioo a b) = Finset.Ioo a (min b c)

ink

@[simp]

theorem Finset.Iio_filter_lt {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrderBot α] (a : α) (b : α) : Finset.filter (fun x => x < b) (Finset.Iio a) = Finset.Iio (min a b)

ink

@[simp]

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

ink

@[simp]

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

ink

theorem Finset.Ioi_disjUnion_Iio {α : Type u_1} [inst : LinearOrder α] [inst : Fintype α] [inst : LocallyFiniteOrderTop α] [inst : LocallyFiniteOrderBot α] (a : α) : Finset.disjUnion (Finset.Ioi a) (Finset.Iio a) (_ : Disjoint (Finset.Ioi a) (Finset.Iio a)) = {a}ᶜ

ink

theorem Finset.uIcc_toDual {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] (a : α) (b : α) : Finset.uIcc (↑OrderDual.toDual a) (↑OrderDual.toDual b) = Finset.map (Equiv.toEmbedding OrderDual.toDual) (Finset.uIcc a b)

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

theorem Finset.uIcc_subset_uIcc {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (h₁ : a₁ ∈ Finset.uIcc a₂ b₂) (h₂ : b₁ ∈ Finset.uIcc a₂ b₂) : Finset.uIcc a₁ b₁ ⊆ Finset.uIcc a₂ b₂

ink

theorem Finset.uIcc_subset_Icc {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} (ha : a₁ ∈ Finset.Icc a₂ b₂) (hb : b₁ ∈ Finset.Icc a₂ b₂) : Finset.uIcc a₁ b₁ ⊆ Finset.Icc a₂ b₂

ink

theorem Finset.uIcc_subset_uIcc_iff_mem {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} : Finset.uIcc a₁ b₁ ⊆ Finset.uIcc a₂ b₂ ↔ a₁ ∈ Finset.uIcc a₂ b₂ ∧ b₁ ∈ Finset.uIcc a₂ b₂

ink

theorem Finset.uIcc_subset_uIcc_iff_le' {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} : Finset.uIcc a₁ b₁ ⊆ Finset.uIcc a₂ b₂ ↔ a₂ ⊓ b₂ ≤ a₁ ⊓ b₁ ∧ a₁ ⊔ b₁ ≤ a₂ ⊔ b₂

ink

theorem Finset.uIcc_subset_uIcc_right {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {x : α} (h : x ∈ Finset.uIcc a b) : Finset.uIcc x b ⊆ Finset.uIcc a b

ink

theorem Finset.uIcc_subset_uIcc_left {α : Type u_1} [inst : Lattice α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {x : α} (h : x ∈ Finset.uIcc a b) : Finset.uIcc a x ⊆ Finset.uIcc a b

ink

theorem Finset.eq_of_mem_uIcc_of_mem_uIcc {α : Type u_1} [inst : DistribLattice α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} : a ∈ Finset.uIcc b c → b ∈ Finset.uIcc a c → a = b

ink

theorem Finset.eq_of_mem_uIcc_of_mem_uIcc' {α : Type u_1} [inst : DistribLattice α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} : b ∈ Finset.uIcc a c → c ∈ Finset.uIcc a b → b = c

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

theorem Finset.not_mem_uIcc_of_lt {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} : c < a → c < b → ¬c ∈ Finset.uIcc a b

ink

theorem Finset.not_mem_uIcc_of_gt {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} : a < c → b < c → ¬c ∈ Finset.uIcc a b

ink

theorem Finset.uIcc_subset_uIcc_iff_le {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a₁ : α} {a₂ : α} {b₁ : α} {b₂ : α} : Finset.uIcc a₁ b₁ ⊆ Finset.uIcc a₂ b₂ ↔ min a₂ b₂ ≤ min a₁ b₁ ∧ max a₁ b₁ ≤ max a₂ b₂

ink

theorem Finset.uIcc_subset_uIcc_union_uIcc {α : Type u_1} [inst : LinearOrder α] [inst : LocallyFiniteOrder α] {a : α} {b : α} {c : α} : Finset.uIcc a c ⊆ Finset.uIcc a b ∪ Finset.uIcc b c

A sort of triangle inequality.

ink

@[simp]

theorem Finset.map_add_left_Icc {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) : Finset.map (addLeftEmbedding c) (Finset.Icc a b) = Finset.Icc (c + a) (c + b)

ink

@[simp]

theorem Finset.map_add_right_Icc {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) : Finset.map (addRightEmbedding c) (Finset.Icc a b) = Finset.Icc (a + c) (b + c)

ink

@[simp]

theorem Finset.map_add_left_Ico {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) : Finset.map (addLeftEmbedding c) (Finset.Ico a b) = Finset.Ico (c + a) (c + b)

ink

@[simp]

theorem Finset.map_add_right_Ico {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) : Finset.map (addRightEmbedding c) (Finset.Ico a b) = Finset.Ico (a + c) (b + c)

ink

@[simp]

theorem Finset.map_add_left_Ioc {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) : Finset.map (addLeftEmbedding c) (Finset.Ioc a b) = Finset.Ioc (c + a) (c + b)

ink

@[simp]

theorem Finset.map_add_right_Ioc {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) : Finset.map (addRightEmbedding c) (Finset.Ioc a b) = Finset.Ioc (a + c) (b + c)

ink

@[simp]

theorem Finset.map_add_left_Ioo {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) : Finset.map (addLeftEmbedding c) (Finset.Ioo a b) = Finset.Ioo (c + a) (c + b)

ink

@[simp]

theorem Finset.map_add_right_Ioo {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] (a : α) (b : α) (c : α) : Finset.map (addRightEmbedding c) (Finset.Ioo a b) = Finset.Ioo (a + c) (b + c)

ink

@[simp]

theorem Finset.image_add_left_Icc {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) (c : α) : Finset.image ((fun x x_1 => x + x_1) c) (Finset.Icc a b) = Finset.Icc (c + a) (c + b)

ink

@[simp]

theorem Finset.image_add_left_Ico {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) (c : α) : Finset.image ((fun x x_1 => x + x_1) c) (Finset.Ico a b) = Finset.Ico (c + a) (c + b)

ink

@[simp]

theorem Finset.image_add_left_Ioc {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) (c : α) : Finset.image ((fun x x_1 => x + x_1) c) (Finset.Ioc a b) = Finset.Ioc (c + a) (c + b)

ink

@[simp]

theorem Finset.image_add_left_Ioo {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) (c : α) : Finset.image ((fun x x_1 => x + x_1) c) (Finset.Ioo a b) = Finset.Ioo (c + a) (c + b)

ink

@[simp]

theorem Finset.image_add_right_Icc {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) (c : α) : Finset.image (fun x => x + c) (Finset.Icc a b) = Finset.Icc (a + c) (b + c)

ink

theorem Finset.image_add_right_Ico {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) (c : α) : Finset.image (fun x => x + c) (Finset.Ico a b) = Finset.Ico (a + c) (b + c)

ink

theorem Finset.image_add_right_Ioc {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) (c : α) : Finset.image (fun x => x + c) (Finset.Ioc a b) = Finset.Ioc (a + c) (b + c)

ink

theorem Finset.image_add_right_Ioo {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] [inst : ExistsAddOfLE α] [inst : LocallyFiniteOrder α] [inst : DecidableEq α] (a : α) (b : α) (c : α) : Finset.image (fun x => x + c) (Finset.Ioo a b) = Finset.Ioo (a + c) (b + c)

ink

theorem Finset.sum_sum_Ioi_add_eq_sum_sum_off_diag {ι : Type u_1} {α : Type u_2} [inst : Fintype ι] [inst : LinearOrder ι] [inst : LocallyFiniteOrderTop ι] [inst : LocallyFiniteOrderBot ι] [inst : AddCommMonoid α] (f : ι → ι → α) : (Finset.sum Finset.univ fun i => Finset.sum (Finset.Ioi i) fun j => f j i + f i j) = Finset.sum Finset.univ fun i => Finset.sum ({i}ᶜ) fun j => f j i

ink

theorem Finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag {ι : Type u_1} {α : Type u_2} [inst : Fintype ι] [inst : LinearOrder ι] [inst : LocallyFiniteOrderTop ι] [inst : LocallyFiniteOrderBot ι] [inst : CommMonoid α] (f : ι → ι → α) : (Finset.prod Finset.univ fun i => Finset.prod (Finset.Ioi i) fun j => f j i * f i j) = Finset.prod Finset.univ fun i => Finset.prod ({i}ᶜ) fun j => f j i