Measurable

📁 Source: Mathlib/Analysis/Calculus/FDeriv/Measurable.lean

Statistics

Metric	Count
Definitions A, B, D, A, B, D	6
Theorems measurable_apply₂, A_mono, D_subset_differentiable_set, differentiable_set_eq_D, differentiable_set_subset_D, isOpen_A, isOpen_A_with_param, isOpen_B, isOpen_B_with_param, le_of_mem_A, mem_A_of_differentiable, norm_sub_le_of_mem_A, A_mem_nhdsGT, A_mono, B_mem_nhdsGT, D_subset_differentiable_set, differentiable_set_eq_D, differentiable_set_subset_D, le_of_mem_A, measurableSet_B, mem_A_of_differentiable, norm_sub_le_of_mem_A, aemeasurable_deriv, aemeasurable_derivWithin_Ici, aemeasurable_derivWithin_Ioi, aemeasurable_deriv_with_param, aestronglyMeasurable_deriv, aestronglyMeasurable_derivWithin_Ici, aestronglyMeasurable_derivWithin_Ioi, aestronglyMeasurable_deriv_with_param, measurableSet_of_differentiableAt, measurableSet_of_differentiableAt_of_isComplete, measurableSet_of_differentiableAt_of_isComplete_with_param, measurableSet_of_differentiableAt_with_param, measurableSet_of_differentiableWithinAt_Ici, measurableSet_of_differentiableWithinAt_Ici_of_isComplete, measurableSet_of_differentiableWithinAt_Ioi, measurable_deriv, measurable_derivWithin_Ici, measurable_derivWithin_Ioi, measurable_deriv_with_param, measurable_fderiv, measurable_fderiv_apply_const, measurable_fderiv_apply_const_with_param, measurable_fderiv_with_param, stronglyMeasurable_deriv, stronglyMeasurable_derivWithin_Ici, stronglyMeasurable_derivWithin_Ioi, stronglyMeasurable_deriv_with_param	49
Total	55

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measurable_apply₂ 📖	mathematical	—	Measurable ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Prod.instMeasurableSpace instMeasurableSpace DFunLike.coe funLike	—	SeminormedAddCommGroup.toIsTopologicalAddGroup Continuous.measurable RingHomIsometric.ids Prod.opensMeasurableSpace BorelSpace.opensMeasurable instBorelSpace IsBoundedBilinearMap.continuous smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul isBoundedBilinearMap_apply

FDerivMeasurableAux

Definitions

Name	Category	Theorems
A 📖	CompOp	4 math math: isOpen_A, isOpen_A_with_param, mem_A_of_differentiable, A_mono
B 📖	CompOp	2 math math: isOpen_B_with_param, isOpen_B
D 📖	CompOp	3 math math: differentiable_set_subset_D, D_subset_differentiable_set, differentiable_set_eq_D

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
A_mono 📖	mathematical	Real Real.instLE	Set Set.instHasSubset A	—	LT.lt.trans_le mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing 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.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_zero 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt 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_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Metric.mem_ball Mathlib.Tactic.Linarith.sub_nonpos_of_le dist_nonneg
D_subset_differentiable_set 📖	mathematical	IsComplete ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.uniformSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.to_isUniformAddGroup	Set Set.instHasSubset D setOf DifferentiableAt NormedAddCommGroup.toAddCommGroup AddCommGroup.toAddCommMonoid Set.instMembership fderiv	—	SeminormedAddCommGroup.to_isUniformAddGroup Nat.instAtLeastTwoHAddOfNat pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.instAtLeastTwo NormedField.exists_one_lt_norm Set.mem_iInter Set.mem_iUnion SeminormedAddCommGroup.toIsTopologicalAddGroup pow_le_pow_of_le_one IsOrderedRing.toPosMulMono Real.instIsOrderedRing Mathlib.Meta.NormNum.isRat_le_true Mathlib.Meta.NormNum.IsNNRat.to_isRat le_max_left norm_sub_le_of_mem_A le_max_right A_mono IsTopologicalAddGroup.toContinuousAdd Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add RingHomIsometric.ids Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Abel.zero_termg Mathlib.Tactic.Abel.const_add_termg add_zero norm_add₃_le add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_zero_add Metric.cauchySeq_iff' exists_pow_lt_of_lt_one Real.instArchimedean AddGroup.existsAddOfLE div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE mul_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial lt_trans dist_comm dist_eq_norm le_rfl mul_lt_mul_of_pos_left Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ one_mul Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Meta.NormNum.isNat_eq_false ne_of_gt Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial cauchySeq_tendsto_of_isComplete le_of_tendsto instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.norm Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub ContinuousLinearMap.topologicalAddGroup tendsto_const_nhds Filter.eventually_atTop add_pos' Metric.eventually_nhds_iff_ball sub_self map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass norm_zero MulZeroClass.mul_zero norm_pos_iff one_div inv_pow sub_zero mem_ball_iff_norm le_trans LT.lt.le pow_le_one₀ exists_nat_pow_near_of_lt_one pow_lt_pow_iff_right_of_lt_one₀ lt_of_le_of_lt zero_le Nat.instCanonicallyOrderedAdd le_of_mem_A dist_self le_of_lt IsStrictOrderedRing.toZeroLEOneClass add_sub_cancel_left pow_succ mul_one_div Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.isNNRat_pow Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Meta.NormNum.one_natPow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Meta.NormNum.IsNNRat.to_isNat mul_le_mul_of_nonneg_left sub_add_sub_cancel norm_add_le_of_le LE.le.trans ContinuousLinearMap.le_opNorm mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ HasFDerivAt.differentiableAt HasFDerivAt.fderiv IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Function.sometimes_spec
differentiable_set_eq_D 📖	mathematical	IsComplete ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.uniformSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.to_isUniformAddGroup	setOf DifferentiableAt NormedAddCommGroup.toAddCommGroup AddCommGroup.toAddCommMonoid Set Set.instMembership fderiv D	—	SeminormedAddCommGroup.to_isUniformAddGroup Set.Subset.antisymm differentiable_set_subset_D D_subset_differentiable_set
differentiable_set_subset_D 📖	mathematical	—	Set Set.instHasSubset setOf DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Set.instMembership fderiv D	—	D.eq_1 Set.mem_iInter Nat.instAtLeastTwoHAddOfNat pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsStrictOrderedRing.toZeroLEOneClass div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.instAtLeastTwo mem_A_of_differentiable exists_pow_lt_of_lt_one Real.instArchimedean AddGroup.existsAddOfLE Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Set.iInter_congr_Prop lt_of_le_of_lt pow_le_pow_of_le_one IsOrderedRing.toPosMulMono Mathlib.Meta.NormNum.isRat_le_true Mathlib.Meta.NormNum.IsNNRat.to_isRat Nat.cast_zero
isOpen_A 📖	mathematical	—	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup A	—	Metric.isOpen_iff Nat.instAtLeastTwoHAddOfNat exists_between LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing le_of_lt LT.lt.trans_le lt_of_not_ge 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.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_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_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Metric.ball_subset
isOpen_A_with_param 📖	mathematical	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	IsOpen setOf Set Set.instMembership A	—	ProperSpace.of_locallyCompactSpace map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass isOpen_iff_mem_nhds exists_between LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Continuous.norm Continuous.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup Continuous.comp' Continuous.prodMk continuous_const continuous_id' Continuous.snd Continuous.fst Continuous.clm_apply le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Nat.instAtLeastTwoHAddOfNat 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.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.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_neg 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 CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Meta.NormNum.isNat_lt_true IsCompact.exists_isMaxOn instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid IsCompact.prod ProperSpace.isCompact_closedBall Continuous.continuousOn LE.le.trans_lt Set.mem_prod lt_of_not_ge Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Linarith.add_lt_of_neg_of_le CancelDenoms.mul_subst Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Meta.NormNum.IsNat.to_raw_eq CancelDenoms.add_subst Uniform.exists_is_open_mem_uniformity_of_forall_mem_eq Continuous.continuousAt Metric.dist_mem_uniformity generalized_tube_lemma isCompact_singleton prod_mem_nhds IsOpen.mem_nhds Metric.ball_mem_nhds sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Filter.mp_mem Filter.univ_mem' LE.le.trans LT.lt.le dist_triangle Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Tactic.Abel.zero_termg norm_add₃_le add_le_add dist_eq_norm dist_eq_norm' Mathlib.Meta.NormNum.isNat_add
isOpen_B 📖	mathematical	—	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup B	—	—
isOpen_B_with_param 📖	mathematical	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	IsOpen setOf Set Set.instMembership B	—	isOpen_biUnion IsOpen.inter isOpen_A_with_param Set.ext
le_of_mem_A 📖	mathematical	Set Set.instMembership A Metric.closedBall SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	Real.instLE Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.funLike Real.instMul	—	Nat.instAtLeastTwoHAddOfNat le_of_lt LE.le.trans_lt Metric.mem_closedBall
mem_A_of_differentiable 📖	mathematical	Real Real.instLT Real.instZero DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	Set Set.instMembership A fderiv SeminormedAddCommGroup.toAddCommGroup	—	Nat.instAtLeastTwoHAddOfNat Metric.eventually_nhds_iff_ball Asymptotics.IsLittleO.bound HasFDerivAtFilter.isLittleO DifferentiableAt.hasFDerivAt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Set.right_mem_Ioc half_lt_self map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Abel.termg_eq one_zsmul add_zero Mathlib.Tactic.Abel.const_add_termg Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Abel.zero_termg norm_sub_le add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Metric.ball_subset_ball LT.lt.le mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono le_of_lt mem_ball_iff_norm Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNNRat_add Mathlib.Tactic.Ring.add_pf_zero_add mul_lt_mul_of_pos_right IsStrictOrderedRing.toMulPosStrictMono
norm_sub_le_of_mem_A 📖	mathematical	Real Real.instLT Real.instOne Norm.norm NormedField.toNorm NontriviallyNormedField.toNormedField Real.instZero Set Set.instMembership A	Real.instLE ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.hasOpNorm ContinuousLinearMap.sub NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	ContinuousLinearMap.opNorm_le_of_shell RingHomIsometric.ids SeminormedAddCommGroup.toIsTopologicalAddGroup Nat.instAtLeastTwoHAddOfNat half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing le_of_lt mul_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo lt_trans Nat.cast_one add_sub_cancel_left sub_sub_sub_cancel_left norm_sub_le add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add le_of_mem_A dist_self dist_eq_norm LT.lt.le Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.mul_one mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono div_le_iff₀' div_div Mathlib.Meta.NormNum.isNat_mul

RightDerivMeasurableAux

Definitions

Name	Category	Theorems
A 📖	CompOp	2 math math: A_mono, mem_A_of_differentiable
B 📖	CompOp	1 math math: measurableSet_B
D 📖	CompOp	3 math math: D_subset_differentiable_set, differentiable_set_subset_D, differentiable_set_eq_D

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
A_mem_nhdsGT 📖	mathematical	Real Set Set.instMembership A	Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ioi Real.instPreorder	—	Nat.instAtLeastTwoHAddOfNat exists_between LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing le_of_lt LT.lt.trans_le Filter.mp_mem Ioo_mem_nhdsGT instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid lt_of_not_ge 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.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.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Filter.univ_mem' Set.Icc_subset_Icc LT.lt.le le_of_not_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Linarith.add_neg
A_mono 📖	mathematical	Real Real.instLE	Set Set.instHasSubset A	—	LE.le.trans mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing 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.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_zero 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt 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_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Linarith.sub_nonpos_of_le
B_mem_nhdsGT 📖	mathematical	Real Set Set.instMembership B	Filter Filter.instMembership nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ioi Real.instPreorder	—	Filter.mp_mem A_mem_nhdsGT Filter.univ_mem'
D_subset_differentiable_set 📖	mathematical	IsComplete PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	Set Real Set.instHasSubset D setOf DifferentiableWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace Real.pseudoMetricSpace NormedAddCommGroup.toAddCommGroup Set.Ici Real.instPreorder Set.instMembership derivWithin	—	Nat.instAtLeastTwoHAddOfNat pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.instAtLeastTwo Set.mem_iInter Set.mem_iUnion pow_le_pow_of_le_one IsOrderedRing.toPosMulMono Real.instIsOrderedRing Mathlib.Meta.NormNum.isRat_le_true Mathlib.Meta.NormNum.IsNNRat.to_isRat le_max_left norm_sub_le_of_mem_A le_max_right A_mono Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Abel.zero_termg Mathlib.Tactic.Abel.const_add_termg add_zero le_imp_le_of_le_of_le norm_add_le le_refl add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid add_le_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_zero_add Metric.cauchySeq_iff' exists_pow_lt_of_lt_one Real.instArchimedean AddGroup.existsAddOfLE div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Mathlib.Meta.NormNum.isNat_lt_true dist_comm dist_eq_norm le_rfl mul_lt_mul' IsOrderedRing.toMulPosMono le_of_lt Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz cauchySeq_tendsto_of_isComplete le_of_tendsto instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.norm Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup tendsto_const_nhds Filter.eventually_atTop IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Filter.mp_mem Icc_mem_nhdsGE instClosedIciTopology one_div inv_pow IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Real.instNontrivial Filter.univ_mem' eq_or_lt_of_le sub_self zero_smul norm_zero MulZeroClass.mul_zero sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_one_cast 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.without_one_mul CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq CancelDenoms.sub_subst Mathlib.Tactic.Linarith.sub_neg_of_lt CancelDenoms.add_subst Mathlib.Tactic.Linarith.sub_nonpos_of_le le_trans pow_le_one₀ exists_nat_pow_near_of_lt_one lt_of_lt_of_le pow_lt_pow_iff_right_of_lt_one₀ lt_of_le_of_lt zero_le Nat.instCanonicallyOrderedAdd le_of_mem_A IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT inv_pos_of_pos IsStrictOrderedRing.toZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat pow_one pow_add AddGroup.toOrderedSub Mathlib.Meta.NormNum.isNNRat_pow Mathlib.Meta.NormNum.one_natPow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 mul_le_mul_of_nonneg_left mul_pos Real.norm_of_nonneg LT.lt.le smul_sub sub_add_sub_cancel norm_add_le_of_le norm_smul NormedSpace.toNormSMulClass norm_nonneg mul_nonneg HasDerivWithinAt.differentiableWithinAt HasDerivWithinAt.derivWithin uniqueDiffOn_Ici Set.self_mem_Ici AddTorsor.nonempty Function.sometimes_spec
differentiable_set_eq_D 📖	mathematical	IsComplete PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	setOf Real DifferentiableWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace Real.pseudoMetricSpace NormedAddCommGroup.toAddCommGroup Set.Ici Real.instPreorder Set Set.instMembership derivWithin D	—	Set.Subset.antisymm differentiable_set_subset_D D_subset_differentiable_set
differentiable_set_subset_D 📖	mathematical	—	Set Real Set.instHasSubset setOf DifferentiableWithinAt 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 NormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Set.Ici Real.instPreorder Set.instMembership derivWithin D	—	D.eq_1 Set.mem_iInter Nat.instAtLeastTwoHAddOfNat pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.instAtLeastTwo mem_A_of_differentiable exists_pow_lt_of_lt_one Real.instArchimedean AddGroup.existsAddOfLE Set.iInter_congr_Prop lt_of_le_of_lt pow_le_pow_of_le_one IsOrderedRing.toPosMulMono Real.instIsOrderedRing Mathlib.Meta.NormNum.isRat_le_true Mathlib.Meta.NormNum.IsNNRat.to_isRat
le_of_mem_A 📖	mathematical	Real Set Set.instMembership A Set.Icc Real.instPreorder Real.instAdd DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	Real.instLE Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField Real.instSub Real.instMul	—	Nat.instAtLeastTwoHAddOfNat le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Nat.cast_one Mathlib.Tactic.Ring.one_mul 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_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_neg Real.instIsStrictOrderedRing CancelDenoms.sub_subst CancelDenoms.add_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true Set.Icc_subset_Icc le_rfl
measurableSet_B 📖	mathematical	—	MeasurableSet Real Real.measurableSpace B	—	MeasurableSet.of_mem_nhdsGT Real.borelSpace instOrderTopologyReal instSecondCountableTopologyReal B_mem_nhdsGT
mem_A_of_differentiable 📖	mathematical	Real Real.instLT Real.instZero DifferentiableWithinAt 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 NormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Set.Ici Real.instPreorder	Set Set.instMembership A derivWithin	—	IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul DifferentiableWithinAt.hasDerivWithinAt Nat.instAtLeastTwoHAddOfNat mem_nhdsGE_iff_exists_Ico_subset instOrderTopologyReal instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing lt_of_not_ge 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_zero Mathlib.Tactic.Ring.add_pf_add_gt 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 Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt half_lt_self le_rfl sub_smul Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.const_add_termg Mathlib.Tactic.Abel.term_add_termg Mathlib.Tactic.Abel.zero_termg norm_sub_le add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add LE.le.trans_lt Mathlib.Meta.NormNum.IsNat.to_raw_eq mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.norm_of_nonneg le_of_not_gt Mathlib.Tactic.Linarith.add_lt_of_neg_of_le le_of_lt div_pos Mathlib.Meta.Positivity.pos_of_isNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz
norm_sub_le_of_mem_A 📖	mathematical	Real Real.instLT Real.instZero Set Set.instMembership A	Real.instLE Norm.norm NormedAddCommGroup.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat smul_sub add_sub_cancel_left sub_sub_sub_cancel_left norm_sub_le add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add le_of_mem_A IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le LT.lt.le half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz mul_le_mul_iff_right₀ IsOrderedRing.toPosMulMono Real.instIsOrderedRing Real.norm_of_nonneg norm_smul NormedSpace.toNormSMulClass

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aemeasurable_deriv 📖	mathematical	—	AEMeasurable deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	Measurable.aemeasurable measurable_deriv
aemeasurable_derivWithin_Ici 📖	mathematical	—	AEMeasurable Real Real.measurableSpace derivWithin DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set.Ici Real.instPreorder	—	Measurable.aemeasurable measurable_derivWithin_Ici
aemeasurable_derivWithin_Ioi 📖	mathematical	—	AEMeasurable Real Real.measurableSpace derivWithin DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set.Ioi Real.instPreorder	—	Measurable.aemeasurable measurable_derivWithin_Ioi
aemeasurable_deriv_with_param 📖	mathematical	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	AEMeasurable Prod.instMeasurableSpace deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule	—	Measurable.aemeasurable measurable_deriv_with_param
aestronglyMeasurable_deriv 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField	—	MeasureTheory.StronglyMeasurable.aestronglyMeasurable stronglyMeasurable_deriv
aestronglyMeasurable_derivWithin_Ici 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.measurableSpace derivWithin DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Set.Ici Real.instPreorder	—	MeasureTheory.StronglyMeasurable.aestronglyMeasurable stronglyMeasurable_derivWithin_Ici
aestronglyMeasurable_derivWithin_Ioi 📖	mathematical	—	MeasureTheory.AEStronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.measurableSpace derivWithin DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Set.Ioi Real.instPreorder	—	MeasureTheory.StronglyMeasurable.aestronglyMeasurable stronglyMeasurable_derivWithin_Ioi
aestronglyMeasurable_deriv_with_param 📖	mathematical	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	MeasureTheory.AEStronglyMeasurable Prod.instMeasurableSpace deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule	—	MeasureTheory.StronglyMeasurable.aestronglyMeasurable stronglyMeasurable_deriv_with_param
measurableSet_of_differentiableAt 📖	mathematical	—	MeasurableSet setOf DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	SeminormedAddCommGroup.to_isUniformAddGroup complete_univ ContinuousLinearMap.instCompleteSpace SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul FrechetUrysohnSpace.to_sequentialSpace FirstCountableTopology.frechetUrysohnSpace TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace measurableSet_of_differentiableAt_of_isComplete
measurableSet_of_differentiableAt_of_isComplete 📖	mathematical	IsComplete ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.uniformSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.to_isUniformAddGroup	MeasurableSet setOf DifferentiableAt NormedAddCommGroup.toAddCommGroup AddCommGroup.toAddCommMonoid Set Set.instMembership fderiv	—	SeminormedAddCommGroup.to_isUniformAddGroup FDerivMeasurableAux.differentiable_set_eq_D Set.iInter_congr_Prop one_div inv_pow MeasurableSet.iInter instCountableNat MeasurableSet.iUnion Prop.countable IsOpen.measurableSet FDerivMeasurableAux.isOpen_B
measurableSet_of_differentiableAt_of_isComplete_with_param 📖	mathematical	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup IsComplete ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule ContinuousLinearMap.uniformSpace SeminormedAddCommGroup.toAddCommGroup SeminormedAddCommGroup.to_isUniformAddGroup	MeasurableSet Prod.instMeasurableSpace setOf DifferentiableAt NormedAddCommGroup.toAddCommGroup AddCommGroup.toAddCommMonoid Set Set.instMembership fderiv	—	SeminormedAddCommGroup.to_isUniformAddGroup FDerivMeasurableAux.differentiable_set_eq_D Set.setOf_forall Set.setOf_exists Set.iInter_congr_Prop MeasurableSet.iInter instCountableNat MeasurableSet.iUnion Prop.countable ProperSpace.of_locallyCompactSpace IsOpen.measurableSet Prod.opensMeasurableSpace secondCountableTopologyEither_of_right secondCountable_of_proper FDerivMeasurableAux.isOpen_B_with_param
measurableSet_of_differentiableAt_with_param 📖	mathematical	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	MeasurableSet Prod.instMeasurableSpace setOf DifferentiableAt NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField	—	SeminormedAddCommGroup.to_isUniformAddGroup complete_univ ContinuousLinearMap.instCompleteSpace SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul FrechetUrysohnSpace.to_sequentialSpace FirstCountableTopology.frechetUrysohnSpace TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace measurableSet_of_differentiableAt_of_isComplete_with_param
measurableSet_of_differentiableWithinAt_Ici 📖	mathematical	—	MeasurableSet Real Real.measurableSpace setOf DifferentiableWithinAt 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 NormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Set.Ici Real.instPreorder	—	complete_univ measurableSet_of_differentiableWithinAt_Ici_of_isComplete
measurableSet_of_differentiableWithinAt_Ici_of_isComplete 📖	mathematical	IsComplete PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	MeasurableSet Real Real.measurableSpace setOf DifferentiableWithinAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace Real.pseudoMetricSpace NormedAddCommGroup.toAddCommGroup Set.Ici Real.instPreorder Set Set.instMembership derivWithin	—	RightDerivMeasurableAux.differentiable_set_eq_D MeasurableSet.iInter instCountableNat MeasurableSet.iUnion Prop.countable RightDerivMeasurableAux.measurableSet_B
measurableSet_of_differentiableWithinAt_Ioi 📖	mathematical	—	MeasurableSet Real Real.measurableSpace setOf DifferentiableWithinAt 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 NormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddCommGroup.toPseudoMetricSpace Set.Ioi Real.instPreorder	—	measurableSet_of_differentiableWithinAt_Ici
measurable_deriv 📖	mathematical	—	Measurable deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace	—	measurable_fderiv_apply_const
measurable_derivWithin_Ici 📖	mathematical	—	Measurable Real Real.measurableSpace derivWithin DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set.Ici Real.instPreorder	—	measurable_of_isClosed Set.ext Set.mem_preimage derivWithin_mem_iff MeasurableSet.union measurableSet_of_differentiableWithinAt_Ici_of_isComplete IsClosed.isComplete MeasurableSet.inter MeasurableSet.compl measurableSet_of_differentiableWithinAt_Ici MeasurableSet.const
measurable_derivWithin_Ioi 📖	mathematical	—	Measurable Real Real.measurableSpace derivWithin DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Set.Ioi Real.instPreorder	—	derivWithin_Ioi_eq_Ici measurable_derivWithin_Ici
measurable_deriv_with_param 📖	mathematical	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	Measurable Prod.instMeasurableSpace deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule	—	measurable_fderiv_apply_const_with_param
measurable_fderiv 📖	mathematical	—	Measurable ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousLinearMap.instMeasurableSpace fderiv	—	measurable_of_isClosed SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.instBorelSpace Set.ext Set.mem_preimage fderiv_mem_iff MeasurableSet.union measurableSet_of_differentiableAt_of_isComplete IsClosed.isComplete SeminormedAddCommGroup.to_isUniformAddGroup ContinuousLinearMap.instCompleteSpace IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul FrechetUrysohnSpace.to_sequentialSpace FirstCountableTopology.frechetUrysohnSpace TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace MeasurableSet.inter MeasurableSet.compl measurableSet_of_differentiableAt MeasurableSet.const
measurable_fderiv_apply_const 📖	mathematical	—	Measurable DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousLinearMap.funLike fderiv	—	Measurable.comp ContinuousLinearMap.measurable_apply measurable_fderiv
measurable_fderiv_apply_const_with_param 📖	mathematical	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	Measurable Prod.instMeasurableSpace DFunLike.coe ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule ContinuousLinearMap.funLike fderiv	—	Measurable.comp ContinuousLinearMap.measurable_apply measurable_fderiv_with_param
measurable_fderiv_with_param 📖	mathematical	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	Measurable ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Prod.instMeasurableSpace ContinuousLinearMap.instMeasurableSpace fderiv	—	measurable_of_isClosed SeminormedAddCommGroup.toIsTopologicalAddGroup ContinuousLinearMap.instBorelSpace Set.ext Set.mem_preimage fderiv_mem_iff MeasurableSet.union measurableSet_of_differentiableAt_of_isComplete_with_param IsClosed.isComplete SeminormedAddCommGroup.to_isUniformAddGroup ContinuousLinearMap.instCompleteSpace IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul FrechetUrysohnSpace.to_sequentialSpace FirstCountableTopology.frechetUrysohnSpace TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace MeasurableSet.inter MeasurableSet.compl measurableSet_of_differentiableAt_with_param MeasurableSet.const
stronglyMeasurable_deriv 📖	mathematical	—	MeasureTheory.StronglyMeasurable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NontriviallyNormedField.toNormedField	—	SecondCountableTopologyEither.out stronglyMeasurable_iff_measurable_separable PseudoEMetricSpace.pseudoMetrizableSpace measurable_deriv isSeparable_range_deriv TopologicalSpace.SecondCountableTopology.to_separableSpace Measurable.stronglyMeasurable BorelSpace.opensMeasurable
stronglyMeasurable_derivWithin_Ici 📖	mathematical	—	MeasureTheory.StronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.measurableSpace derivWithin DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Set.Ici Real.instPreorder	—	stronglyMeasurable_iff_measurable_separable PseudoEMetricSpace.pseudoMetrizableSpace measurable_derivWithin_Ici TopologicalSpace.exists_countable_dense TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal range_derivWithin_subset_closure_span_image dense_iff_closure_eq Set.inter_univ closure_Ioi instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial closure_mono Set.inter_comm IsOpen.closure_inter isOpen_Ioi instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid closure_closure Set.inter_subset_inter_left Set.Ioi_subset_Ici_self Set.mem_range_self TopologicalSpace.IsSeparable.mono TopologicalSpace.IsSeparable.closure TopologicalSpace.IsSeparable.span IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Set.Countable.isSeparable Set.Countable.image
stronglyMeasurable_derivWithin_Ioi 📖	mathematical	—	MeasureTheory.StronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Real.measurableSpace derivWithin DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField Set.Ioi Real.instPreorder	—	derivWithin_Ioi_eq_Ici stronglyMeasurable_derivWithin_Ici
stronglyMeasurable_deriv_with_param 📖	mathematical	Continuous instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup	MeasureTheory.StronglyMeasurable Prod.instMeasurableSpace deriv NormedAddCommGroup.toAddCommGroup NormedSpace.toModule	—	SecondCountableTopologyEither.out ProperSpace.of_locallyCompactSpace stronglyMeasurable_iff_measurable_separable PseudoEMetricSpace.pseudoMetrizableSpace measurable_deriv_with_param Set.image_univ range_deriv_subset_closure_span_image dense_univ Set.mem_range_self closure_mono Submodule.span_mono TopologicalSpace.IsSeparable.mono TopologicalSpace.IsSeparable.closure TopologicalSpace.IsSeparable.span TopologicalSpace.SecondCountableTopology.to_separableSpace secondCountable_of_proper IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul TopologicalSpace.isSeparable_range TopologicalSpace.instSeparableSpaceProd Measurable.stronglyMeasurable BorelSpace.opensMeasurable

---

← Back to Index