Slope

📁 Source: Mathlib/MeasureTheory/Integral/IntervalIntegral/Slope.lean

Statistics

Metric	Count
Definitions	0
Theorems intervalIntegrable_slope, intervalIntegrable_slope, intervalIntegral_slope_le	3
Total	3

IntervalIntegrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
intervalIntegrable_slope 📖	mathematical	IntervalIntegrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instAdd Real.instLE Real.instZero	slope Real.instField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor	—	add_sub_cancel_left const_mul sub mono_set PseudoEMetricSpace.pseudoMetrizableSpace comp_add_right enorm_ne_top

MonotoneOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
intervalIntegrable_slope 📖	mathematical	MonotoneOn Real Real.instPreorder Set.Icc Real.instAdd Real.instLE Real.instZero	IntervalIntegrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup slope Real.instField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor MeasureTheory.MeasureSpace.volume Real.measureSpace	—	IntervalIntegrable.intervalIntegrable_slope intervalIntegrable Real.locallyFinite_volume instOrderTopologyReal instSecondCountableTopologyReal Set.uIcc_of_le 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_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_nonpos Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt
intervalIntegral_slope_le 📖	mathematical	MonotoneOn Real Real.instPreorder Set.Icc Real.instAdd Real.instLE Real.instZero	intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal slope Real.instField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedAddTorsor.toAddTorsor SeminormedAddCommGroup.toPseudoMetricSpace SeminormedAddCommGroup.toNormedAddTorsor MeasureTheory.MeasureSpace.volume Real.measureSpace Real.instSub	—	eq_or_lt_of_le add_zero slope_same intervalIntegral.integral_zero covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid intervalIntegrable Real.locallyFinite_volume instOrderTopologyReal instSecondCountableTopologyReal Set.uIcc_of_le 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_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt add_sub_cancel_left intervalIntegral.integral_const_mul intervalIntegral.integral_sub IntervalIntegrable.mono_set PseudoEMetricSpace.pseudoMetrizableSpace IntervalIntegrable.comp_add_right enorm_ne_top intervalIntegral.integral_comp_add_right intervalIntegral.integral_interval_sub_interval_comm' le_imp_le_of_le_of_le intervalIntegral.integral_mono_on le_refl intervalIntegral.integral_const Real.instCompleteSpace mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono sub_le_sub_right le_of_lt inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono sub_le_sub_left Mathlib.Tactic.FieldSimp.le_eq_cancel_le PosMulStrictMono.toPosMulMono Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt zero_lt_one Real.instZeroLEOneClass NeZero.one GroupWithZero.toNontrivial

---

← Back to Index