mathlib3 documentation

data.fin.interval

Finite intervals in fin n #

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

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

@[simp, norm_cast]
theorem fin.coe_sup {n : } (a b : fin n) :
(a b) = a b
@[simp, norm_cast]
theorem fin.coe_inf {n : } (a b : fin n) :
(a b) = a b
@[simp, norm_cast]
theorem fin.coe_max {n : } (a b : fin n) :
@[simp, norm_cast]
theorem fin.coe_min {n : } (a b : fin n) :
@[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_uIcc {n : } (a b : fin n) :
@[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_fintype_uIcc {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) :