mathlib documentation

data.fin.interval

Finite intervals in `fin n` #

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

@[protected, instance]

def fin.locally_finite_order (n : ℕ) :

locally_finite_order (fin n)

Equations

fin.locally_finite_order n = subtype.locally_finite_order (λ (i : ℕ), i < n)

theorem fin.Icc_eq_finset_subtype {n : ℕ} (a b : fin n) :

finset.Icc a b = finset.subtype (λ (x : ℕ), x < n) (finset.Icc ↑a ↑b)

theorem fin.Ico_eq_finset_subtype {n : ℕ} (a b : fin n) :

finset.Ico a b = finset.subtype (λ (x : ℕ), x < n) (finset.Ico ↑a ↑b)

theorem fin.Ioc_eq_finset_subtype {n : ℕ} (a b : fin n) :

finset.Ioc a b = finset.subtype (λ (x : ℕ), x < n) (finset.Ioc ↑a ↑b)

theorem fin.Ioo_eq_finset_subtype {n : ℕ} (a b : fin n) :

finset.Ioo a b = finset.subtype (λ (x : ℕ), x < n) (finset.Ioo ↑a ↑b)

@[simp]

theorem fin.map_subtype_embedding_Icc {n : ℕ} (a b : fin n) :

finset.map (function.embedding.subtype (λ (i : ℕ), i < n)) (finset.Icc a b) = finset.Icc ↑a ↑b

@[simp]

theorem fin.map_subtype_embedding_Ico {n : ℕ} (a b : fin n) :

finset.map (function.embedding.subtype (λ (i : ℕ), i < n)) (finset.Ico a b) = finset.Ico ↑a ↑b

@[simp]

theorem fin.map_subtype_embedding_Ioc {n : ℕ} (a b : fin n) :

finset.map (function.embedding.subtype (λ (i : ℕ), i < n)) (finset.Ioc a b) = finset.Ioc ↑a ↑b

@[simp]

theorem fin.map_subtype_embedding_Ioo {n : ℕ} (a b : fin n) :

finset.map (function.embedding.subtype (λ (i : ℕ), i < n)) (finset.Ioo a b) = finset.Ioo ↑a ↑b

@[simp]

theorem fin.card_Icc {n : ℕ} (a b : fin n) :

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

@[simp]

theorem fin.card_Ico {n : ℕ} (a b : fin n) :

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

@[simp]

theorem fin.card_Ioc {n : ℕ} (a b : fin n) :

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

@[simp]

theorem fin.card_Ioo {n : ℕ} (a b : fin n) :

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

@[simp]

theorem fin.card_fintype_Icc {n : ℕ} (a b : fin n) :

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

@[simp]

theorem fin.card_fintype_Ico {n : ℕ} (a b : fin n) :

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

@[simp]

theorem fin.card_fintype_Ioc {n : ℕ} (a b : fin n) :

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

@[simp]

theorem fin.card_fintype_Ioo {n : ℕ} (a b : fin n) :

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

theorem fin.Ici_eq_finset_subtype {n : ℕ} (a : fin (n + 1)) :

finset.Ici a = finset.subtype (λ (x : ℕ), x < n + 1) (finset.Icc ↑a (n + 1))

theorem fin.Ioi_eq_finset_subtype {n : ℕ} (a : fin (n + 1)) :

finset.Ioi a = finset.subtype (λ (x : ℕ), x < n + 1) (finset.Ioc ↑a (n + 1))

theorem fin.Iic_eq_finset_subtype {n : ℕ} (b : fin (n + 1)) :

finset.Iic b = finset.subtype (λ (x : ℕ), x < n + 1) (finset.Iic ↑b)

theorem fin.Iio_eq_finset_subtype {n : ℕ} (b : fin (n + 1)) :

finset.Iio b = finset.subtype (λ (x : ℕ), x < n + 1) (finset.Iio ↑b)

@[simp]

theorem fin.map_subtype_embedding_Ici {n : ℕ} (a : fin (n + 1)) :

finset.map (function.embedding.subtype (λ (i : ℕ), i < n + 1)) (finset.Ici a) = finset.Icc ↑a n

@[simp]

theorem fin.map_subtype_embedding_Ioi {n : ℕ} (a : fin (n + 1)) :

finset.map (function.embedding.subtype (λ (i : ℕ), i < n + 1)) (finset.Ioi a) = finset.Ioc ↑a n

@[simp]

theorem fin.map_subtype_embedding_Iic {n : ℕ} (b : fin (n + 1)) :

finset.map (function.embedding.subtype (λ (i : ℕ), i < n + 1)) (finset.Iic b) = finset.Iic ↑b

@[simp]

theorem fin.map_subtype_embedding_Iio {n : ℕ} (b : fin (n + 1)) :

finset.map (function.embedding.subtype (λ (i : ℕ), i < n + 1)) (finset.Iio b) = finset.Iio ↑b

@[simp]

theorem fin.card_Ici {n : ℕ} (a : fin (n + 1)) :

(finset.Ici a).card = n + 1 - ↑a

@[simp]

theorem fin.card_Ioi {n : ℕ} (a : fin (n + 1)) :

(finset.Ioi a).card = n - ↑a

@[simp]

theorem fin.card_Iic {n : ℕ} (b : fin (n + 1)) :

(finset.Iic b).card = ↑b + 1

@[simp]

theorem fin.card_Iio {n : ℕ} (b : fin (n + 1)) :

(finset.Iio b).card = ↑b

@[simp]

theorem fin.card_fintype_Ici {n : ℕ} (a : fin (n + 1)) :

fintype.card ↥(set.Ici a) = n + 1 - ↑a

@[simp]

theorem fin.card_fintype_Ioi {n : ℕ} (a : fin (n + 1)) :

fintype.card ↥(set.Ioi a) = n - ↑a

@[simp]

theorem fin.card_fintype_Iic {n : ℕ} (b : fin (n + 1)) :

fintype.card ↥(set.Iic b) = ↑b + 1

@[simp]

theorem fin.card_fintype_Iio {n : ℕ} (b : fin (n + 1)) :

fintype.card ↥(set.Iio b) = ↑b