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.

source
@[simp, norm_cast]
theorem fin.coe_sup {n : ℕ} (a b : fin n) :
↑(a ⊔ b) = ↑a ⊔ ↑b
source
@[simp, norm_cast]
theorem fin.coe_inf {n : ℕ} (a b : fin n) :
↑(a ⊓ b) = ↑a ⊓ ↑b
source
@[simp, norm_cast]
theorem fin.coe_max {n : ℕ} (a b : fin n) :
↑(linear_order.max a b) = linear_order.max ↑a ↑b
source
@[simp, norm_cast]
theorem fin.coe_min {n : ℕ} (a b : fin n) :
↑(linear_order.min a b) = linear_order.min ↑a ↑b
source
@[protected, instance]
def fin.locally_finite_order (n : ℕ) :
locally_finite_order (fin n)
Equations
source
@[protected, instance]
def fin.locally_finite_order_bot (n : ℕ) :
locally_finite_order_bot (fin n)
Equations
source
@[protected, instance]
def fin.locally_finite_order_top (n : ℕ) :
locally_finite_order_top (fin n)
Equations
source
theorem fin.Icc_eq_finset_subtype {n : ℕ} (a b : fin n) :
finset.Icc a b = finset.fin n (finset.Icc ↑a ↑b)
source
theorem fin.Ico_eq_finset_subtype {n : ℕ} (a b : fin n) :
finset.Ico a b = finset.fin n (finset.Ico ↑a ↑b)
source
theorem fin.Ioc_eq_finset_subtype {n : ℕ} (a b : fin n) :
finset.Ioc a b = finset.fin n (finset.Ioc ↑a ↑b)
source
theorem fin.Ioo_eq_finset_subtype {n : ℕ} (a b : fin n) :
finset.Ioo a b = finset.fin n (finset.Ioo ↑a ↑b)
source
theorem fin.uIcc_eq_finset_subtype {n : ℕ} (a b : fin n) :
finset.uIcc a b = finset.fin n (finset.uIcc ↑a ↑b)
source
@[simp]
theorem fin.map_subtype_embedding_Icc {n : ℕ} (a b : fin n) :
finset.map fin.coe_embedding (finset.Icc a b) = finset.Icc ↑a ↑b
source
@[simp]
theorem fin.map_subtype_embedding_Ico {n : ℕ} (a b : fin n) :
finset.map fin.coe_embedding (finset.Ico a b) = finset.Ico ↑a ↑b
source
@[simp]
theorem fin.map_subtype_embedding_Ioc {n : ℕ} (a b : fin n) :
finset.map fin.coe_embedding (finset.Ioc a b) = finset.Ioc ↑a ↑b
source
@[simp]
theorem fin.map_subtype_embedding_Ioo {n : ℕ} (a b : fin n) :
finset.map fin.coe_embedding (finset.Ioo a b) = finset.Ioo ↑a ↑b
source
@[simp]
theorem fin.map_subtype_embedding_uIcc {n : ℕ} (a b : fin n) :
finset.map fin.coe_embedding (finset.uIcc a b) = finset.uIcc ↑a ↑b
source
@[simp]
theorem fin.card_Icc {n : ℕ} (a b : fin n) :
(finset.Icc a b).card = ↑b + 1 - ↑a
source
@[simp]
theorem fin.card_Ico {n : ℕ} (a b : fin n) :
(finset.Ico a b).card = ↑b - ↑a
source
@[simp]
theorem fin.card_Ioc {n : ℕ} (a b : fin n) :
(finset.Ioc a b).card = ↑b - ↑a
source
@[simp]
theorem fin.card_Ioo {n : ℕ} (a b : fin n) :
(finset.Ioo a b).card = ↑b - ↑a - 1
source
@[simp]
theorem fin.card_uIcc {n : ℕ} (a b : fin n) :
(finset.uIcc a b).card = (↑b - ↑a).nat_abs + 1
source
@[simp]
theorem fin.card_fintype_Icc {n : ℕ} (a b : fin n) :
fintype.card ↥(set.Icc a b) = ↑b + 1 - ↑a
source
@[simp]
theorem fin.card_fintype_Ico {n : ℕ} (a b : fin n) :
fintype.card ↥(set.Ico a b) = ↑b - ↑a
source
@[simp]
theorem fin.card_fintype_Ioc {n : ℕ} (a b : fin n) :
fintype.card ↥(set.Ioc a b) = ↑b - ↑a
source
@[simp]
theorem fin.card_fintype_Ioo {n : ℕ} (a b : fin n) :
fintype.card ↥(set.Ioo a b) = ↑b - ↑a - 1
source
@[simp]
theorem fin.card_fintype_uIcc {n : ℕ} (a b : fin n) :
fintype.card ↥(set.uIcc a b) = (↑b - ↑a).nat_abs + 1
source
theorem fin.Ici_eq_finset_subtype {n : ℕ} (a : fin n) :
finset.Ici a = finset.fin n (finset.Icc ↑a n)
source
theorem fin.Ioi_eq_finset_subtype {n : ℕ} (a : fin n) :
finset.Ioi a = finset.fin n (finset.Ioc ↑a n)
source
theorem fin.Iic_eq_finset_subtype {n : ℕ} (b : fin n) :
finset.Iic b = finset.fin n (finset.Iic ↑b)
source
theorem fin.Iio_eq_finset_subtype {n : ℕ} (b : fin n) :
finset.Iio b = finset.fin n (finset.Iio ↑b)
source
@[simp]
theorem fin.map_subtype_embedding_Ici {n : ℕ} (a : fin n) :
finset.map fin.coe_embedding (finset.Ici a) = finset.Icc ↑a (n - 1)
source
@[simp]
theorem fin.map_subtype_embedding_Ioi {n : ℕ} (a : fin n) :
finset.map fin.coe_embedding (finset.Ioi a) = finset.Ioc ↑a (n - 1)
source
@[simp]
theorem fin.map_subtype_embedding_Iic {n : ℕ} (b : fin n) :
finset.map fin.coe_embedding (finset.Iic b) = finset.Iic ↑b
source
@[simp]
theorem fin.map_subtype_embedding_Iio {n : ℕ} (b : fin n) :
finset.map fin.coe_embedding (finset.Iio b) = finset.Iio ↑b
source
@[simp]
theorem fin.card_Ici {n : ℕ} (a : fin n) :
(finset.Ici a).card = n - ↑a
source
@[simp]
theorem fin.card_Ioi {n : ℕ} (a : fin n) :
(finset.Ioi a).card = n - 1 - ↑a
source
@[simp]
theorem fin.card_Iic {n : ℕ} (b : fin n) :
(finset.Iic b).card = ↑b + 1
source
@[simp]
theorem fin.card_Iio {n : ℕ} (b : fin n) :
(finset.Iio b).card = ↑b
source
@[simp]
theorem fin.card_fintype_Ici {n : ℕ} (a : fin n) :
fintype.card ↥(set.Ici a) = n - ↑a
source
@[simp]
theorem fin.card_fintype_Ioi {n : ℕ} (a : fin n) :
fintype.card ↥(set.Ioi a) = n - 1 - ↑a
source
@[simp]
theorem fin.card_fintype_Iic {n : ℕ} (b : fin n) :
fintype.card ↥(set.Iic b) = ↑b + 1
source
@[simp]
theorem fin.card_fintype_Iio {n : ℕ} (b : fin n) :
fintype.card ↥(set.Iio b) = ↑b