Documentation Verification Report

SmoothTransition

📁 Source: Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean

Statistics

Metric	Count
Definitions `smoothTransition`, `expNegInvGlue`	2
Theorems `contDiff`, `contDiffAt`, `continuous`, `continuousAt`, `eq_one_iff_one_le`, `le_one`, `lt_one_of_lt_one`, `monotone`, `nonneg`, `one`, `one_of_one_le`, `pos_denom`, `pos_of_pos`, `projIcc`, `zero`, `zero_iff_nonpos`, `zero_of_nonpos`, `contDiff`, `contDiff_polynomial_eval_inv_mul`, `continuous_polynomial_eval_inv_mul`, `differentiable_polynomial_eval_inv_mul`, `hasDerivAt_polynomial_eval_inv_mul`, `monotone`, `nonneg`, `not_analyticAt_zero`, `pos_of_pos`, `tendsto_polynomial_inv_mul_zero`, `zero`, `zero_iff_nonpos`, `zero_of_nonpos`	30
Total	32

Real

Definitions

Name	Category	Theorems
`smoothTransition` 📖	CompOp	16 math math: `smoothTransition.eq_one_iff_one_le`, `smoothTransition.zero_of_nonpos`, `smoothTransition.one`, `smoothTransition.one_of_one_le`, `smoothTransition.zero`, `smoothTransition.contDiffAt`, `smoothTransition.lt_one_of_lt_one`, `smoothTransition.le_one`, `smoothTransition.continuousAt`, `smoothTransition.nonneg`, `smoothTransition.pos_of_pos`, `smoothTransition.continuous`, `smoothTransition.zero_iff_nonpos`, `smoothTransition.projIcc`, `smoothTransition.monotone`, `smoothTransition.contDiff`

Real.smoothTransition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiff` 📖	mathematical	—	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `WithTop.some` `ENat` `Real.smoothTransition`	—	`ContDiff.div` `expNegInvGlue.contDiff` `ContDiff.add` `ContDiff.comp` `ContDiff.sub` `contDiff_const` `contDiff_id` `LT.lt.ne'` `pos_denom`
`contDiffAt` 📖	mathematical	—	`ContDiffAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `WithTop.some` `ENat` `Real.smoothTransition`	—	`ContDiff.contDiffAt` `contDiff`
`continuous` 📖	mathematical	—	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.smoothTransition`	—	`ContDiff.continuous` `contDiff`
`continuousAt` 📖	mathematical	—	`ContinuousAt` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.smoothTransition`	—	`Continuous.continuousAt` `continuous`
`eq_one_iff_one_le` 📖	mathematical	—	`Real.smoothTransition` `Real` `Real.instOne` `Real.instLE`	—	`le_or_gt` `one_of_one_le` `LT.lt.ne` `lt_one_of_lt_one`
`le_one` 📖	mathematical	—	`Real` `Real.instLE` `Real.smoothTransition` `Real.instOne`	—	`div_le_one` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `pos_denom` `le_add_of_nonneg_right` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `expNegInvGlue.nonneg`
`lt_one_of_lt_one` 📖	mathematical	`Real` `Real.instLT` `Real.instOne`	`Real.smoothTransition`	—	`div_lt_one` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `pos_denom` `lt_add_of_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `expNegInvGlue.pos_of_pos` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add`
`monotone` 📖	mathematical	—	`Monotone` `Real` `Real.instPreorder` `Real.smoothTransition`	—	`div_le_div_iff₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `pos_denom` `mul_add` `Distrib.leftDistribClass` `mul_comm` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `expNegInvGlue.monotone` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `expNegInvGlue.nonneg`
`nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `Real.smoothTransition`	—	`div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `expNegInvGlue.nonneg` `LT.lt.le` `pos_denom`
`one` 📖	mathematical	—	`Real.smoothTransition` `Real` `Real.instOne`	—	`one_of_one_le` `le_rfl`
`one_of_one_le` 📖	mathematical	`Real` `Real.instLE` `Real.instOne`	`Real.smoothTransition`	—	`div_eq_one_iff_eq` `LT.lt.ne'` `pos_denom` `expNegInvGlue.zero_of_nonpos` `sub_nonpos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `add_zero`
`pos_denom` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `Real.instAdd` `expNegInvGlue` `Real.instSub` `Real.instOne`	—	`LT.lt.gt_or_lt` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `add_pos_of_pos_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `expNegInvGlue.pos_of_pos` `expNegInvGlue.nonneg` `add_pos_of_nonneg_of_pos` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add`
`pos_of_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Real.smoothTransition`	—	`div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `expNegInvGlue.pos_of_pos` `pos_denom`
`projIcc` 📖	mathematical	—	`Real.smoothTransition` `Real` `Set` `Set.instMembership` `Set.Icc` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Real.linearOrder` `Real.instZero` `Real.instOne` `Set.projIcc` `zero_le_one` `Preorder.toLE` `Real.instZeroLEOneClass`	—	`zero_le_one` `Real.instZeroLEOneClass` `Set.IccExtend_eq_self` `zero` `zero_of_nonpos` `LT.lt.le` `one` `one_of_one_le`
`zero` 📖	mathematical	—	`Real.smoothTransition` `Real` `Real.instZero`	—	`zero_of_nonpos` `le_rfl`
`zero_iff_nonpos` 📖	mathematical	—	`Real.smoothTransition` `Real` `Real.instZero` `Real.instLE`	—	`LT.lt.ne'` `pos_denom`
`zero_of_nonpos` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`Real.smoothTransition`	—	`zero_iff_nonpos`

(root)

Definitions

Name	Category	Theorems
`expNegInvGlue` 📖	CompOp	14 math math: `expNegInvGlue.hasDerivAt_polynomial_eval_inv_mul`, `expNegInvGlue.not_analyticAt_zero`, `expNegInvGlue.pos_of_pos`, `expNegInvGlue.tendsto_polynomial_inv_mul_zero`, `expNegInvGlue.nonneg`, `expNegInvGlue.monotone`, `expNegInvGlue.contDiff`, `expNegInvGlue.continuous_polynomial_eval_inv_mul`, `expNegInvGlue.contDiff_polynomial_eval_inv_mul`, `expNegInvGlue.zero`, `expNegInvGlue.differentiable_polynomial_eval_inv_mul`, `Real.smoothTransition.pos_denom`, `expNegInvGlue.zero_of_nonpos`, `expNegInvGlue.zero_iff_nonpos`

expNegInvGlue

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiff` 📖	mathematical	—	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `WithTop.some` `ENat` `expNegInvGlue`	—	`Polynomial.eval_one` `one_mul` `contDiff_polynomial_eval_inv_mul`
`contDiff_polynomial_eval_inv_mul` 📖	mathematical	—	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `WithTop.some` `ENat` `Real.instMul` `Polynomial.eval` `Real.semiring` `Real.instInv` `expNegInvGlue`	—	`contDiff_all_iff_nat` `contDiff_zero` `continuous_polynomial_eval_inv_mul` `contDiff_succ_iff_deriv` `differentiable_polynomial_eval_inv_mul` `instIsEmptyFalse` `HasDerivAt.deriv` `hasDerivAt_polynomial_eval_inv_mul`
`continuous_polynomial_eval_inv_mul` 📖	mathematical	—	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instMul` `Polynomial.eval` `Real.semiring` `Real.instInv` `expNegInvGlue`	—	`Differentiable.continuous` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `differentiable_polynomial_eval_inv_mul`
`differentiable_polynomial_eval_inv_mul` 📖	mathematical	—	`Differentiable` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instMul` `Polynomial.eval` `Real.semiring` `Real.instInv` `expNegInvGlue`	—	`HasDerivAt.differentiableAt` `hasDerivAt_polynomial_eval_inv_mul`
`hasDerivAt_polynomial_eval_inv_mul` 📖	mathematical	—	`HasDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.instAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ContinuousMul.to_continuousSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `IsTopologicalSemiring.toContinuousMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `instIsTopologicalRingReal` `Real.instMul` `Polynomial.eval` `Real.semiring` `Real.instInv` `expNegInvGlue` `Polynomial` `Polynomial.instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Polynomial.semiring` `Polynomial.X` `Polynomial.instSub` `Real.instRing` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.derivative`	—	`ContinuousMul.to_continuousSMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `lt_trichotomy` `zero_of_nonpos` `LT.lt.le` `MulZeroClass.mul_zero` `HasDerivAt.congr_of_eventuallyEq` `hasDerivAt_const` `Filter.mp_mem` `gt_mem_nhds` `instOrderTopologyReal` `Filter.univ_mem'` `zero` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `hasDerivAt_iff_tendsto_slope` `Filter.Tendsto.congr` `Polynomial.eval_mul` `Polynomial.eval_X` `mul_right_comm` `slope_def_field` `inv_zero` `sub_zero` `div_eq_mul_inv` `Filter.Tendsto.mono_left` `tendsto_polynomial_inv_mul_zero` `inf_le_left` `HasDerivAt.comp` `HasDerivAt.mul` `Polynomial.hasDerivAt` `HasDerivAt.exp` `hasDerivAt_neg` `hasDerivAt_inv` `LT.lt.ne'` `Polynomial.eval_pow` `inv_pow` `Polynomial.eval_sub` `LT.lt.not_ge` `mul_neg` `mul_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.inv_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.IsInt.to_isNat` `lt_mem_nhds`
`monotone` 📖	mathematical	—	`Monotone` `Real` `Real.instPreorder` `expNegInvGlue`	—	`le_or_gt` `zero_of_nonpos` `not_le` `LT.lt.trans_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `inv_le_inv₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono`
`nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `expNegInvGlue`	—	`le_or_gt` `ge_of_eq` `zero_of_nonpos` `le_of_lt` `pos_of_pos`
`not_analyticAt_zero` 📖	mathematical	—	`AnalyticAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField` `expNegInvGlue` `Real.instZero`	—	`AnalyticAt.exists_ball_analyticOnNhd` `Real.instCompleteSpace` `Nat.instAtLeastTwoHAddOfNat` `AnalyticOnNhd.eqOn_zero_of_preconnected_of_mem_closure` `isPreconnected_Ioo` `instOrderTopologyReal` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.ball_eq_Ioo` `dist_self` `Set.Iic_diff_right` `closure_Iio` `instNoMinOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial` `dist_zero_right` `norm_div` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.norm_ofNat`
`pos_of_pos` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`expNegInvGlue`	—	`not_le`
`tendsto_polynomial_inv_mul_zero` 📖	mathematical	—	`Filter.Tendsto` `Real` `Real.instMul` `Polynomial.eval` `Real.semiring` `Real.instInv` `expNegInvGlue` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero`	—	`mul_ite` `MulZeroClass.mul_zero` `Filter.Tendsto.if` `tendsto_const_nhds` `Filter.Tendsto.comp` `Polynomial.tendsto_div_exp_atTop` `tendsto_inv_nhdsGT_zero` `Real.instIsStrictOrderedRing` `instOrderTopologyReal` `Filter.Tendsto.congr'` `Filter.mem_of_superset` `self_mem_nhdsWithin` `div_eq_mul_inv` `Real.exp_neg`
`zero` 📖	mathematical	—	`expNegInvGlue` `Real` `Real.instZero`	—	`zero_of_nonpos` `le_rfl`
`zero_iff_nonpos` 📖	mathematical	—	`expNegInvGlue` `Real` `Real.instZero` `Real.instLE`	—	`not_lt` `LT.lt.ne'` `pos_of_pos` `zero_of_nonpos`
`zero_of_nonpos` 📖	mathematical	`Real` `Real.instLE` `Real.instZero`	`expNegInvGlue`	—	—

---

← Back to Index