SubboxInduction

📁 Source: Mathlib/Analysis/BoxIntegral/Box/SubboxInduction.lean

Statistics

Metric	Count
Definitions splitCenterBox, splitCenterBoxEmb	2
Theorems disjoint_splitCenterBox, exists_mem_splitCenterBox, iUnion_coe_splitCenterBox, injective_splitCenterBox, mem_splitCenterBox, splitCenterBoxEmb_apply, splitCenterBox_le, subbox_induction_on', upper_sub_lower_splitCenterBox	9
Total	11

BoxIntegral.Box

Definitions

Name	Category	Theorems
splitCenterBox 📖	CompOp	9 math math: splitCenterBox_le, disjoint_splitCenterBox, exists_mem_splitCenterBox, upper_sub_lower_splitCenterBox, mem_splitCenterBox, BoxIntegral.Prepartition.mem_splitCenter, iUnion_coe_splitCenterBox, splitCenterBoxEmb_apply, injective_splitCenterBox
splitCenterBoxEmb 📖	CompOp	1 math math: splitCenterBoxEmb_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint_splitCenterBox 📖	mathematical	—	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice toSet splitCenterBox	—	disjoint_iff_inf_le Set.ext Nat.instAtLeastTwoHAddOfNat mem_splitCenterBox mem_coe
exists_mem_splitCenterBox 📖	mathematical	—	BoxIntegral.Box instMembershipForallReal splitCenterBox	—	splitCenterBox_le Nat.instAtLeastTwoHAddOfNat mem_splitCenterBox
iUnion_coe_splitCenterBox 📖	mathematical	—	Set.iUnion Set toSet splitCenterBox	—	Set.ext
injective_splitCenterBox 📖	mathematical	—	Set BoxIntegral.Box splitCenterBox	—	by_contra Disjoint.ne Set.Nonempty.ne_empty nonempty_coe disjoint_splitCenterBox
mem_splitCenterBox 📖	mathematical	—	BoxIntegral.Box instMembershipForallReal splitCenterBox Real Real.instLT DivInvMonoid.toDiv Real.instDivInvMonoid Real.instAdd lower upper instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Set Set.instMembership	—	Nat.instAtLeastTwoHAddOfNat LT.lt.trans left_lt_add_div_two PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing lower_lt_upper LE.le.trans LT.lt.le add_div_two_lt_right
splitCenterBoxEmb_apply 📖	mathematical	—	DFunLike.coe Function.Embedding Set BoxIntegral.Box Function.instFunLikeEmbedding splitCenterBoxEmb splitCenterBox	—	—
splitCenterBox_le 📖	mathematical	—	BoxIntegral.Box instLE splitCenterBox	—	Nat.instAtLeastTwoHAddOfNat mem_splitCenterBox
subbox_induction_on' 📖	—	Set Filter Filter.instMembership nhdsWithin Pi.topologicalSpace Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe OrderEmbedding BoxIntegral.Box instLE Set.instLE instFunLikeOrderEmbedding Icc	—	—	Nat.instAtLeastTwoHAddOfNat not_imp_not Function.iterate_succ_apply' antitone_nat_of_succ_le splitCenterBox_le zero_le Nat.instCanonicallyOrderedAdd pow_zero div_one upper_sub_lower_splitCenterBox div_div pow_succ Set.mem_iInter ciSup_mem_iInter_Icc_of_antitone_Icc instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Monotone.comp_antitone OrderEmbedding.monotone lower_le_upper le_iff_Icc lower_mem_Icc upper_mem_Icc tendsto_atTop_ciSup Pi.supConvergenceClass' LinearOrder.supConvergenceClass instOrderTopologyReal Antitone.comp antitone_lower tendsto_pi_nhds Filter.Tendsto.div_atTop Real.instIsStrictOrderedRing tendsto_const_nhds tendsto_pow_atTop_atTop_of_one_lt AddGroup.existsAddOfLE Real.instArchimedean one_lt_two Real.instZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid add_sub_cancel add_zero Filter.Tendsto.add instContinuousAddForallOfIsTopologicalSemiring IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within Filter.Eventually.of_forall Filter.Eventually.exists Filter.atTop_neBot Filter.tendsto_lift' Filter.Tendsto.Icc tendstoIxxNhdsWithin tendstoIccClassNhdsPi Filter.tendsto_Icc_Icc_Icc Function.sometimes_spec
upper_sub_lower_splitCenterBox 📖	mathematical	—	Real Real.instSub upper splitCenterBox lower DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Set.piecewise_eq_of_mem Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Meta.NormNum.isNat_eq_false IsStrictOrderedRing.toCharZero Real.instIsStrictOrderedRing Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons 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.div_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos 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.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt 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 Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Set.piecewise_eq_of_notMem

---

← Back to Index