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.

@[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) :
@[simp]
theorem fin.card_Ici {n : } (a : fin n) :
@[simp]
theorem fin.card_Ioi {n : } (a : fin n) :
(finset.Ioi a).card = n - 1 - a
@[simp]
theorem fin.card_Iic {n : } (b : fin n) :
@[simp]
theorem fin.card_Iio {n : } (b : fin n) :
@[simp]
theorem fin.card_fintype_Ici {n : } (a : fin n) :
@[simp]
theorem fin.card_fintype_Ioi {n : } (a : fin n) :
@[simp]
theorem fin.card_fintype_Iic {n : } (b : fin n) :
@[simp]
theorem fin.card_fintype_Iio {n : } (b : fin n) :