Cardinalities of intervals

Cardinalities of intervals can be computed using finsets in locally finite orders.

theorem Set.cardinalMk_Icc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Cardinal.mk ↑(Icc a b) = ↑(Finset.Icc a b).card

theorem Set.encard_Icc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : (Icc a b).encard = ↑(Finset.Icc a b).card

theorem Set.ncard_Icc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : (Icc a b).ncard = (Finset.Icc a b).card

theorem Set.cardinalMk_Ico {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Cardinal.mk ↑(Ico a b) = ↑(Finset.Ico a b).card

theorem Set.cardinalMk_Ioc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (b a : α) : Cardinal.mk ↑(Ioc b a) = ↑(Finset.Ioc b a).card

theorem Set.encard_Ico {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : (Ico a b).encard = ↑(Finset.Ico a b).card

theorem Set.encard_Ioc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (b a : α) : (Ioc b a).encard = ↑(Finset.Ioc b a).card

theorem Set.ncard_Ico {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : (Ico a b).ncard = (Finset.Ico a b).card

theorem Set.ncard_Ioc {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (b a : α) : (Ioc b a).ncard = (Finset.Ioc b a).card

theorem Set.cardinalMk_Ioo {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : Cardinal.mk ↑(Ioo a b) = ↑(Finset.Ioo a b).card

theorem Set.encard_Ioo {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : (Ioo a b).encard = ↑(Finset.Ioo a b).card

theorem Set.ncard_Ioo {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] (a b : α) : (Ioo a b).ncard = (Finset.Ioo a b).card

theorem Set.cardinalMk_Ici {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) : Cardinal.mk ↑(Ici a) = ↑(Finset.Ici a).card

theorem Set.cardinalMk_Iic {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : α) : Cardinal.mk ↑(Iic a) = ↑(Finset.Iic a).card

theorem Set.encard_Ici {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) : (Ici a).encard = ↑(Finset.Ici a).card

theorem Set.encard_Iic {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : α) : (Iic a).encard = ↑(Finset.Iic a).card

theorem Set.ncard_Ici {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) : (Ici a).ncard = (Finset.Ici a).card

theorem Set.ncard_Iic {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : α) : (Iic a).ncard = (Finset.Iic a).card

theorem Set.cardinalMk_Ioi {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) : Cardinal.mk ↑(Ioi a) = ↑(Finset.Ioi a).card

theorem Set.cardinalMk_Iio {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : α) : Cardinal.mk ↑(Iio a) = ↑(Finset.Iio a).card

theorem Set.encard_Ioi {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) : (Ioi a).encard = ↑(Finset.Ioi a).card

theorem Set.encard_Iio {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : α) : (Iio a).encard = ↑(Finset.Iio a).card

theorem Set.ncard_Ioi {α : Type u_1} [Preorder α] [LocallyFiniteOrderTop α] (a : α) : (Ioi a).ncard = (Finset.Ioi a).card

theorem Set.ncard_Iio {α : Type u_1} [Preorder α] [LocallyFiniteOrderBot α] (a : α) : (Iio a).ncard = (Finset.Iio a).card

theorem Set.cardinalMk_uIcc {α : Type u_1} [Lattice α] [LocallyFiniteOrder α] (a b : α) : Cardinal.mk ↑(uIcc a b) = ↑(Finset.uIcc a b).card

theorem Set.encard_uIcc {α : Type u_1} [Lattice α] [LocallyFiniteOrder α] (a b : α) : (uIcc a b).encard = ↑(Finset.uIcc a b).card

theorem Set.ncard_uIcc {α : Type u_1} [Lattice α] [LocallyFiniteOrder α] (a b : α) : (uIcc a b).ncard = (Finset.uIcc a b).card