Real

Statistics

Metric	Count
Definitions	0
Theorems `ratSqrt_le_realSqrt`, `ratSqrt_mem_Ioc`, `realSqrt_lt_ratSqrt_add_inv_prec`, `realSqrt_mem_Ico`	4
Total	4

Name	Kind	Assumes	Proves	Validates	Depends On
`ratSqrt_le_realSqrt` 📖	mathematical	—	`Real` `Real.instLE` `Real.instRatCast` `ratSqrt` `Real.sqrt` `Real.instNatCast`	—	`ratSqrt_sq_le` `Real.instIsStrictOrderedRing` `Real.sqrt_monotone` `Real.sqrt_sq` `ratSqrt_nonneg`
`ratSqrt_mem_Ioc` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `Set.Ioc` `Real.instPreorder` `Real.instSub` `Real.sqrt` `Real.instNatCast` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instRatCast` `ratSqrt`	—	—
`realSqrt_lt_ratSqrt_add_inv_prec` 📖	mathematical	—	`Real` `Real.instLT` `Real.sqrt` `Real.instNatCast` `Real.instAdd` `Real.instRatCast` `ratSqrt` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`lt_ratSqrt_add_inv_prec_sq` `cast_one` `Real.instIsStrictOrderedRing` `Real.sqrt_lt_sqrt` `Real.instIsOrderedRing` `Rat.cast_add` `IsStrictOrderedRing.toCharZero` `Rat.cast_div` `Rat.cast_one` `Rat.cast_natCast` `Real.sqrt_sq` `add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `ratSqrt_nonneg` `one_div` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Rat.cast_pow`
`realSqrt_mem_Ico` 📖	mathematical	—	`Real` `Set` `Set.instMembership` `Set.Ico` `Real.instPreorder` `Real.instRatCast` `ratSqrt` `Real.instAdd` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `Real.instNatCast` `Real.sqrt`	—	—

---