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]
Equations
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]
@[simp]
@[simp]
@[simp]
@[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) :
@[simp]
theorem fin.card_Ioc {n : } (a b : fin n) :
@[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) :
@[simp]
theorem fin.card_fintype_Ico {n : } (a b : fin n) :
@[simp]
theorem fin.card_fintype_Ioc {n : } (a b : fin n) :
@[simp]
theorem fin.card_fintype_Ioo {n : } (a b : fin n) :
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)) :
@[simp]
theorem fin.map_subtype_embedding_Ioi {n : } (a : fin (n + 1)) :
@[simp]
theorem fin.map_subtype_embedding_Iic {n : } (b : fin (n + 1)) :
@[simp]
theorem fin.map_subtype_embedding_Iio {n : } (b : fin (n + 1)) :
@[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)) :
@[simp]
theorem fin.card_Iic {n : } (b : fin (n + 1)) :
@[simp]
theorem fin.card_Iio {n : } (b : fin (n + 1)) :
@[simp]
theorem fin.card_fintype_Ici {n : } (a : fin (n + 1)) :
@[simp]
theorem fin.card_fintype_Ioi {n : } (a : fin (n + 1)) :
@[simp]
theorem fin.card_fintype_Iic {n : } (b : fin (n + 1)) :
@[simp]
theorem fin.card_fintype_Iio {n : } (b : fin (n + 1)) :
@[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 nfin n → R} :
finset.univ.prod (λ (i : fin n), (finset.filter (λ (j : fin n), i < j) finset.univ).prod (λ (j : fin n), f j i * f i j)) = finset.univ.prod (λ (i : fin n), (finset.filter (λ (j : fin n), i j) finset.univ).prod (λ (j : fin n), f j i))