SetInterval

📁 Source: Mathlib/Data/Nat/Cast/SetInterval.lean

Statistics

Metric	Count
Definitions	0
Theorems image_cast_int_Icc, image_cast_int_Ici, image_cast_int_Ico, image_cast_int_Iic, image_cast_int_Iio, image_cast_int_Ioc, image_cast_int_Ioi, image_cast_int_Ioo, range_cast_int	9
Total	9

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_cast_int_Icc 📖	mathematical	—	Set.image Set.Icc instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	OrderEmbedding.image_Icc Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero range_cast_int
image_cast_int_Ici 📖	mathematical	—	Set.image Set.Ici instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	OrderEmbedding.image_Ici Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero range_cast_int
image_cast_int_Ico 📖	mathematical	—	Set.image Set.Ico instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	OrderEmbedding.image_Ico Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero range_cast_int
image_cast_int_Iic 📖	mathematical	—	Set.image Set.Iic instPreorder Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	Set.Icc_bot image_cast_int_Icc
image_cast_int_Iio 📖	mathematical	—	Set.image Set.Iio instPreorder Set.Ico PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	Set.Ico_bot image_cast_int_Ico
image_cast_int_Ioc 📖	mathematical	—	Set.image Set.Ioc instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	OrderEmbedding.image_Ioc Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero range_cast_int
image_cast_int_Ioi 📖	mathematical	—	Set.image Set.Ioi instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	OrderEmbedding.image_Ioi Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero range_cast_int
image_cast_int_Ioo 📖	mathematical	—	Set.image Set.Ioo instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	OrderEmbedding.image_Ioo Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero range_cast_int
range_cast_int 📖	mathematical	—	Set.range Set.Ici PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt	—	Set.Subset.antisymm Set.range_subset_iff CanLift.prf instCanLiftIntNatCastLeOfNat

---

← Back to Index