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

@[simp]

theorem fin.card_filter_lt {n : ℕ} (a : fin n) :

(finset.filter (λ (j : fin n), a < j) finset.univ).card = n - ↑a - 1

@[simp]

theorem fin.card_filter_le {n : ℕ} (a : fin n) :

(finset.filter (λ (j : fin n), a ≤ j) finset.univ).card = n - ↑a

@[simp]

theorem fin.card_filter_gt {n : ℕ} (a : fin n) :

(finset.filter (λ (j : fin n), j < a) finset.univ).card = ↑a

@[simp]

theorem fin.card_filter_ge {n : ℕ} (a : fin n) :

(finset.filter (λ (j : fin n), j ≤ a) finset.univ).card = ↑a + 1

@[simp]

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

(finset.filter (λ (j : fin n), a < j ∧ j < b) finset.univ).card = ↑b - ↑a - 1

@[simp]

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

(finset.filter (λ (j : fin n), a < j ∧ j ≤ b) finset.univ).card = ↑b - ↑a

@[simp]

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

(finset.filter (λ (j : fin n), a ≤ j ∧ j < b) finset.univ).card = ↑b - ↑a

@[simp]

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

(finset.filter (λ (j : fin n), a ≤ j ∧ j ≤ b) finset.univ).card = ↑b + 1 - ↑a

theorem fin.prod_filter_lt_mul_neg_eq_prod_off_diag {R : Type u_1} [comm_monoid R] {n : ℕ} {f : fin n → fin n → R} :

∏ (i : fin n), ∏ (j : fin n) in finset.filter (λ (j : fin n), i < j) finset.univ, (f j i) * f i j = ∏ (i : fin n), ∏ (j : fin n) in finset.filter (λ (j : fin n), i ≠ j) finset.univ, f j i