Interval

Statistics

Metric	Count
Definitions	0
Theorems `int_eq_of_mul_mem_Ioo`, `int_mem_Icc_of_mul_mem_Ioo`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`int_eq_of_mul_mem_Ioo` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Set` `Set.instMembership` `Set.Ioo` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	—	—	`Finset.Icc_self` `int_mem_Icc_of_mul_mem_Ioo`
`int_mem_Icc_of_mul_mem_Ioo` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Set` `Set.instMembership` `Set.Ioo` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne`	`Finset` `Finset.instMembership` `Finset.Icc` `instLatticeInt` `Int.instLocallyFiniteOrder`	—	`mul_lt_mul_iff_right₀` `toPosMulStrictMono` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `toIsOrderedRing` `toZeroLEOneClass` `NeZero.charZero_one` `toCharZero`

---