HepLean Documentation

Mathlib.Algebra.Order.Interval.Finset

Algebraic properties of finset intervals #

This file provides results about the interaction of algebra with Finset.Ixx.

source
@[simp]
theorem Finset.map_add_left_Icc {α : Type u_2} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) :
Finset.map (addLeftEmbedding c) (Finset.Icc a b) = Finset.Icc (c + a) (c + b)
source
@[simp]
theorem Finset.map_add_right_Icc {α : Type u_2} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) :
Finset.map (addRightEmbedding c) (Finset.Icc a b) = Finset.Icc (a + c) (b + c)
source
@[simp]
theorem Finset.map_add_left_Ico {α : Type u_2} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) :
Finset.map (addLeftEmbedding c) (Finset.Ico a b) = Finset.Ico (c + a) (c + b)
source
@[simp]
theorem Finset.map_add_right_Ico {α : Type u_2} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) :
Finset.map (addRightEmbedding c) (Finset.Ico a b) = Finset.Ico (a + c) (b + c)
source
@[simp]
theorem Finset.map_add_left_Ioc {α : Type u_2} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) :
Finset.map (addLeftEmbedding c) (Finset.Ioc a b) = Finset.Ioc (c + a) (c + b)
source
@[simp]
theorem Finset.map_add_right_Ioc {α : Type u_2} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) :
Finset.map (addRightEmbedding c) (Finset.Ioc a b) = Finset.Ioc (a + c) (b + c)
source
@[simp]
theorem Finset.map_add_left_Ioo {α : Type u_2} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) :
Finset.map (addLeftEmbedding c) (Finset.Ioo a b) = Finset.Ioo (c + a) (c + b)
source
@[simp]
theorem Finset.map_add_right_Ioo {α : Type u_2} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (a b c : α) :
Finset.map (addRightEmbedding c) (Finset.Ioo a b) = Finset.Ioo (a + c) (b + c)
source
@[simp]
theorem Finset.image_add_left_Icc {α : Type u_2} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [DecidableEq α] (a b c : α) :
Finset.image (fun (x : α) => c + x) (Finset.Icc a b) = Finset.Icc (c + a) (c + b)
source
@[simp]
theorem Finset.image_add_left_Ico {α : Type u_2} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [DecidableEq α] (a b c : α) :
Finset.image (fun (x : α) => c + x) (Finset.Ico a b) = Finset.Ico (c + a) (c + b)
source
@[simp]
theorem Finset.image_add_left_Ioc {α : Type u_2} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [DecidableEq α] (a b c : α) :
Finset.image (fun (x : α) => c + x) (Finset.Ioc a b) = Finset.Ioc (c + a) (c + b)
source
@[simp]
theorem Finset.image_add_left_Ioo {α : Type u_2} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [DecidableEq α] (a b c : α) :
Finset.image (fun (x : α) => c + x) (Finset.Ioo a b) = Finset.Ioo (c + a) (c + b)
source
@[simp]
theorem Finset.image_add_right_Icc {α : Type u_2} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [DecidableEq α] (a b c : α) :
Finset.image (fun (x : α) => x + c) (Finset.Icc a b) = Finset.Icc (a + c) (b + c)
source
@[simp]
theorem Finset.image_add_right_Ico {α : Type u_2} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [DecidableEq α] (a b c : α) :
Finset.image (fun (x : α) => x + c) (Finset.Ico a b) = Finset.Ico (a + c) (b + c)
source
@[simp]
theorem Finset.image_add_right_Ioc {α : Type u_2} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [DecidableEq α] (a b c : α) :
Finset.image (fun (x : α) => x + c) (Finset.Ioc a b) = Finset.Ioc (a + c) (b + c)
source
@[simp]
theorem Finset.image_add_right_Ioo {α : Type u_2} [OrderedCancelAddCommMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [DecidableEq α] (a b c : α) :
Finset.image (fun (x : α) => x + c) (Finset.Ioo a b) = Finset.Ioo (a + c) (b + c)