Finite intervals of integers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves that ℤ is a locally_finite_order and calculates the cardinality of its intervals as finsets and fintypes.

source

@[protected, instance]

def int.locally_finite_order :

locally_finite_order ℤ

Equations

int.locally_finite_order = {finset_Icc := λ (a b : ℤ), finset.map (nat.cast_embedding.trans (add_left_embedding a)) (finset.range (b + 1 - a).to_nat), finset_Ico := λ (a b : ℤ), finset.map (nat.cast_embedding.trans (add_left_embedding a)) (finset.range (b - a).to_nat), finset_Ioc := λ (a b : ℤ), finset.map (nat.cast_embedding.trans (add_left_embedding (a + 1))) (finset.range (b - a).to_nat), finset_Ioo := λ (a b : ℤ), finset.map (nat.cast_embedding.trans (add_left_embedding (a + 1))) (finset.range (b - a - 1).to_nat), finset_mem_Icc := int.locally_finite_order._proof_2, finset_mem_Ico := int.locally_finite_order._proof_3, finset_mem_Ioc := int.locally_finite_order._proof_4, finset_mem_Ioo := int.locally_finite_order._proof_5}

source

theorem int.Icc_eq_finset_map (a b : ℤ) :

finset.Icc a b = finset.map (nat.cast_embedding.trans (add_left_embedding a)) (finset.range (b + 1 - a).to_nat)

source

theorem int.Ico_eq_finset_map (a b : ℤ) :

finset.Ico a b = finset.map (nat.cast_embedding.trans (add_left_embedding a)) (finset.range (b - a).to_nat)

source

theorem int.Ioc_eq_finset_map (a b : ℤ) :

finset.Ioc a b = finset.map (nat.cast_embedding.trans (add_left_embedding (a + 1))) (finset.range (b - a).to_nat)

source

theorem int.Ioo_eq_finset_map (a b : ℤ) :

finset.Ioo a b = finset.map (nat.cast_embedding.trans (add_left_embedding (a + 1))) (finset.range (b - a - 1).to_nat)

source

theorem int.uIcc_eq_finset_map (a b : ℤ) :

finset.uIcc a b = finset.map (nat.cast_embedding.trans (add_left_embedding (linear_order.min a b))) (finset.range (linear_order.max a b + 1 - linear_order.min a b).to_nat)

source

@[simp]

theorem int.card_Icc (a b : ℤ) :

(finset.Icc a b).card = (b + 1 - a).to_nat

source

@[simp]

theorem int.card_Ico (a b : ℤ) :

(finset.Ico a b).card = (b - a).to_nat

source

@[simp]

theorem int.card_Ioc (a b : ℤ) :

(finset.Ioc a b).card = (b - a).to_nat

source

@[simp]

theorem int.card_Ioo (a b : ℤ) :

(finset.Ioo a b).card = (b - a - 1).to_nat

source

@[simp]

theorem int.card_uIcc (a b : ℤ) :

(finset.uIcc a b).card = (b - a).nat_abs + 1

source

theorem int.card_Icc_of_le (a b : ℤ) (h : a ≤ b + 1) :

↑((finset.Icc a b).card) = b + 1 - a

source

theorem int.card_Ico_of_le (a b : ℤ) (h : a ≤ b) :

↑((finset.Ico a b).card) = b - a

source

theorem int.card_Ioc_of_le (a b : ℤ) (h : a ≤ b) :

↑((finset.Ioc a b).card) = b - a

source

theorem int.card_Ioo_of_lt (a b : ℤ) (h : a < b) :

↑((finset.Ioo a b).card) = b - a - 1

source

@[simp]

theorem int.card_fintype_Icc (a b : ℤ) :

fintype.card ↥(set.Icc a b) = (b + 1 - a).to_nat

source

@[simp]

theorem int.card_fintype_Ico (a b : ℤ) :

fintype.card ↥(set.Ico a b) = (b - a).to_nat

source

@[simp]

theorem int.card_fintype_Ioc (a b : ℤ) :

fintype.card ↥(set.Ioc a b) = (b - a).to_nat

source

@[simp]

theorem int.card_fintype_Ioo (a b : ℤ) :

fintype.card ↥(set.Ioo a b) = (b - a - 1).to_nat

source

@[simp]

theorem int.card_fintype_uIcc (a b : ℤ) :

fintype.card ↥(set.uIcc a b) = (b - a).nat_abs + 1

source

theorem int.card_fintype_Icc_of_le (a b : ℤ) (h : a ≤ b + 1) :

↑(fintype.card ↥(set.Icc a b)) = b + 1 - a

source

theorem int.card_fintype_Ico_of_le (a b : ℤ) (h : a ≤ b) :

↑(fintype.card ↥(set.Ico a b)) = b - a

source

theorem int.card_fintype_Ioc_of_le (a b : ℤ) (h : a ≤ b) :

↑(fintype.card ↥(set.Ioc a b)) = b - a

source

theorem int.card_fintype_Ioo_of_lt (a b : ℤ) (h : a < b) :

↑(fintype.card ↥(set.Ioo a b)) = b - a - 1

source

theorem int.image_Ico_mod (n a : ℤ) (h : 0 ≤ a) :

finset.image (λ (_x : ℤ), _x % a) (finset.Ico n (n + a)) = finset.Ico 0 a