# Documentation

Mathlib.Data.Fin.Interval

# Finite intervals in Fin n#

This file proves that Fin n is a LocallyFiniteOrder and calculates the cardinality of its intervals as Finsets and Fintypes.

@[simp]
theorem Fin.coe_sup {n : } (a : Fin n) (b : Fin n) :
↑(a b) = a b
@[simp]
theorem Fin.coe_inf {n : } (a : Fin n) (b : Fin n) :
↑(a b) = a b
@[simp]
theorem Fin.coe_max {n : } (a : Fin n) (b : Fin n) :
↑(max a b) = max a b
@[simp]
theorem Fin.coe_min {n : } (a : Fin n) (b : Fin n) :
↑(min a b) = min a b
theorem Fin.Icc_eq_finset_subtype {n : } (a : Fin n) (b : Fin n) :
= Finset.fin n (Finset.Icc a b)
theorem Fin.Ico_eq_finset_subtype {n : } (a : Fin n) (b : Fin n) :
= Finset.fin n (Finset.Ico a b)
theorem Fin.Ioc_eq_finset_subtype {n : } (a : Fin n) (b : Fin n) :
= Finset.fin n (Finset.Ioc a b)
theorem Fin.Ioo_eq_finset_subtype {n : } (a : Fin n) (b : Fin n) :
= Finset.fin n (Finset.Ioo a b)
theorem Fin.uIcc_eq_finset_subtype {n : } (a : Fin n) (b : Fin n) :
= Finset.fin n (Finset.uIcc a b)
@[simp]
theorem Fin.map_valEmbedding_Icc {n : } (a : Fin n) (b : Fin n) :
Finset.map Fin.valEmbedding () = Finset.Icc a b
@[simp]
theorem Fin.map_valEmbedding_Ico {n : } (a : Fin n) (b : Fin n) :
Finset.map Fin.valEmbedding () = Finset.Ico a b
@[simp]
theorem Fin.map_valEmbedding_Ioc {n : } (a : Fin n) (b : Fin n) :
Finset.map Fin.valEmbedding () = Finset.Ioc a b
@[simp]
theorem Fin.map_valEmbedding_Ioo {n : } (a : Fin n) (b : Fin n) :
Finset.map Fin.valEmbedding () = Finset.Ioo a b
@[simp]
theorem Fin.map_subtype_embedding_uIcc {n : } (a : Fin n) (b : Fin n) :
Finset.map Fin.valEmbedding () = Finset.uIcc a b
@[simp]
theorem Fin.card_Icc {n : } (a : Fin n) (b : Fin n) :
Finset.card () = b + 1 - a
@[simp]
theorem Fin.card_Ico {n : } (a : Fin n) (b : Fin n) :
Finset.card () = b - a
@[simp]
theorem Fin.card_Ioc {n : } (a : Fin n) (b : Fin n) :
Finset.card () = b - a
@[simp]
theorem Fin.card_Ioo {n : } (a : Fin n) (b : Fin n) :
Finset.card () = b - a - 1
@[simp]
theorem Fin.card_uIcc {n : } (a : Fin n) (b : Fin n) :
Finset.card () = Int.natAbs (b - a) + 1
theorem Fin.card_fintypeIcc {n : } (a : Fin n) (b : Fin n) :
Fintype.card ↑(Set.Icc a b) = b + 1 - a
theorem Fin.card_fintypeIco {n : } (a : Fin n) (b : Fin n) :
Fintype.card ↑(Set.Ico a b) = b - a
theorem Fin.card_fintypeIoc {n : } (a : Fin n) (b : Fin n) :
Fintype.card ↑(Set.Ioc a b) = b - a
theorem Fin.card_fintypeIoo {n : } (a : Fin n) (b : Fin n) :
Fintype.card ↑(Set.Ioo a b) = b - a - 1
theorem Fin.card_fintype_uIcc {n : } (a : Fin n) (b : Fin n) :
Fintype.card ↑(Set.uIcc a b) = Int.natAbs (b - a) + 1
theorem Fin.Ici_eq_finset_subtype {n : } (a : Fin n) :
= Finset.fin n (Finset.Icc (a) n)
theorem Fin.Ioi_eq_finset_subtype {n : } (a : Fin n) :
= Finset.fin n (Finset.Ioc (a) n)
theorem Fin.Iic_eq_finset_subtype {n : } (b : Fin n) :
theorem Fin.Iio_eq_finset_subtype {n : } (b : Fin n) :
@[simp]
theorem Fin.map_valEmbedding_Ici {n : } (a : Fin n) :
Finset.map Fin.valEmbedding () = Finset.Icc (a) (n - 1)
@[simp]
theorem Fin.map_valEmbedding_Ioi {n : } (a : Fin n) :
Finset.map Fin.valEmbedding () = Finset.Ioc (a) (n - 1)
@[simp]
theorem Fin.map_valEmbedding_Iic {n : } (b : Fin n) :
Finset.map Fin.valEmbedding () =
@[simp]
theorem Fin.map_valEmbedding_Iio {n : } (b : Fin n) :
Finset.map Fin.valEmbedding () =
@[simp]
theorem Fin.card_Ici {n : } (a : Fin n) :
= n - a
@[simp]
theorem Fin.card_Ioi {n : } (a : Fin n) :
= n - 1 - a
@[simp]
theorem Fin.card_Iic {n : } (b : Fin n) :
= b + 1
@[simp]
theorem Fin.card_Iio {n : } (b : Fin n) :
= b
theorem Fin.card_fintypeIci {n : } (a : Fin n) :
Fintype.card ↑() = n - a
theorem Fin.card_fintypeIoi {n : } (a : Fin n) :
Fintype.card ↑() = n - 1 - a
theorem Fin.card_fintypeIic {n : } (b : Fin n) :
Fintype.card ↑() = b + 1
theorem Fin.card_fintypeIio {n : } (b : Fin n) :
Fintype.card ↑() = b