PartialTraj

📁 Source: Mathlib/Probability/Kernel/IonescuTulcea/PartialTraj.lean

Statistics

Metric	Count
Definitions lmarginalPartialTraj, partialTraj	2
Theorems dependsOn_lmarginalPartialTraj, lmarginalPartialTraj_const_right, lmarginalPartialTraj_of_le, instIsFiniteKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat, instIsMarkovKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat, instIsSFiniteKernelForallValNatMemFinsetIicPartialTraj, instIsZeroOrMarkovKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat, lmarginalPartialTraj_eq_lintegral_map, lmarginalPartialTraj_le, lmarginalPartialTraj_mono, lmarginalPartialTraj_self, lmarginalPartialTraj_succ, map_partialTraj_succ_self, measurable_lmarginalPartialTraj, partialTraj_comp_partialTraj, partialTraj_comp_partialTraj', partialTraj_comp_partialTraj'', partialTraj_eq_prod, partialTraj_le, partialTraj_le_def, partialTraj_map_frestrictLe₂, partialTraj_map_frestrictLe₂_apply, partialTraj_self, partialTraj_succ_eq_comp, partialTraj_succ_map_frestrictLe₂, partialTraj_succ_of_le, partialTraj_succ_self, partialTraj_zero	28
Total	30

DependsOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dependsOn_lmarginalPartialTraj 📖	mathematical	ProbabilityTheory.IsSFiniteKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder DependsOn ENNReal SetLike.coe Measurable ENNReal.measurableSpace	ProbabilityTheory.Kernel.lmarginalPartialTraj	—	le_total ProbabilityTheory.Kernel.lmarginalPartialTraj_le Finset.Iic_subset_Iic Finset.Ioc_subset_Iic_self ProbabilityTheory.Kernel.lmarginalPartialTraj_eq_lintegral_map updateFinset Finset.coe_sdiff Finset.Iic_diff_Ioc_self_of_le
lmarginalPartialTraj_const_right 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Measurable ENNReal ENNReal.measurableSpace DependsOn SetLike.coe	ProbabilityTheory.Kernel.lmarginalPartialTraj	—	le_total ProbabilityTheory.Kernel.lmarginalPartialTraj_self lmarginalPartialTraj_of_le LE.le.trans le_of_not_ge
lmarginalPartialTraj_of_le 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Measurable ENNReal ENNReal.measurableSpace DependsOn SetLike.coe	ProbabilityTheory.Kernel.lmarginalPartialTraj	—	Finset.Ioc_subset_Iic_self ProbabilityTheory.Kernel.lmarginalPartialTraj_eq_lintegral_map ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel MeasureTheory.lintegral_eq_const ProbabilityTheory.IsMarkovKernel.isProbabilityMeasure ProbabilityTheory.Kernel.IsMarkovKernel.map ProbabilityTheory.Kernel.instIsMarkovKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat Finset.measurable_restrict₂ MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass Finset.coe_Iic

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
lmarginalPartialTraj 📖	CompOp	10 math math: DependsOn.lmarginalPartialTraj_of_le, lmarginalPartialTraj_self, DependsOn.lmarginalPartialTraj_const_right, lmarginalPartialTraj_le, DependsOn.dependsOn_lmarginalPartialTraj, measurable_lmarginalPartialTraj, lmarginalPartialTraj_mono, trajContent_eq_lmarginalPartialTraj, lmarginalPartialTraj_succ, lmarginalPartialTraj_eq_lintegral_map
partialTraj 📖	CompOp	34 math math: partialTraj_succ_of_le, condExp_traj', trajContent_cylinder, partialTraj_comp_partialTraj', map_partialTraj_succ_self, partialTraj_comp_partialTraj'', aestronglyMeasurable_traj, partialTraj_compProd_traj, partialTraj_succ_eq_comp, partialTraj_le_def, traj_comp_partialTraj, partialTraj_map_frestrictLe₂_apply, instIsSFiniteKernelForallValNatMemFinsetIicPartialTraj, partialTraj_succ_map_frestrictLe₂, MeasureTheory.partialTraj_const, partialTraj_le, partialTraj_succ_self, isProjectiveLimit_trajFun, instIsFiniteKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat, partialTraj_comp_partialTraj, integral_traj_partialTraj, instIsZeroOrMarkovKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat, isProjectiveMeasureFamily_partialTraj, partialTraj_self, traj_map_frestrictLe, traj_map_frestrictLe_apply, MeasureTheory.partialTraj_const_restrict₂, setIntegral_traj_partialTraj, partialTraj_map_frestrictLe₂, partialTraj_zero, lmarginalPartialTraj_eq_lintegral_map, partialTraj_compProd_eq_map_traj, partialTraj_eq_prod, instIsMarkovKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsFiniteKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat 📖	mathematical	ProbabilityTheory.IsFiniteKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	partialTraj	—	le_total Nat.le_induction partialTraj_self ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelId partialTraj_succ_of_le IsFiniteKernel.map IsFiniteKernel.comp IsFiniteKernel.prod Preorder.measurable_frestrictLe₂ partialTraj_le isMarkovKernel_deterministic
instIsMarkovKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	partialTraj	—	le_total Nat.le_induction partialTraj_self instIsMarkovKernelId partialTraj_succ_of_le IsMarkovKernel.map MeasurableEquiv.measurable IsMarkovKernel.comp IsMarkovKernel.prod measurable_IicProdIoc Preorder.measurable_frestrictLe₂ partialTraj_le isMarkovKernel_deterministic
instIsSFiniteKernelForallValNatMemFinsetIicPartialTraj 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder partialTraj	—	le_total Nat.le_induction partialTraj_self IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelId partialTraj_succ_of_le IsSFiniteKernel.map IsSFiniteKernel.comp IsSFiniteKernel.prod Preorder.measurable_frestrictLe₂ partialTraj_le isMarkovKernel_deterministic
instIsZeroOrMarkovKernelForallValNatMemFinsetIicPartialTrajOfHAddOfNat 📖	mathematical	ProbabilityTheory.IsZeroOrMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	partialTraj	—	le_total Nat.le_induction partialTraj_self ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelId partialTraj_succ_of_le IsZeroOrMarkovKernel.map IsZeroOrMarkovKernel.comp IsZeroOrMarkovKernel.prod Preorder.measurable_frestrictLe₂ partialTraj_le isMarkovKernel_deterministic
lmarginalPartialTraj_eq_lintegral_map 📖	mathematical	ProbabilityTheory.IsSFiniteKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Measurable ENNReal ENNReal.measurableSpace	lmarginalPartialTraj MeasureTheory.lintegral Finset.Ioc DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike map partialTraj Finset.restrict₂ Finset.Ioc_subset_Iic_self Preorder.frestrictLe Function.updateFinset	—	Finset.Ioc_subset_Iic_self lmarginalPartialTraj.eq_1 partialTraj_eq_prod lintegral_map measurable_IicProdIoc Measurable.fun_comp measurable_updateFinset lintegral_id_prod IsSFiniteKernel.map instIsSFiniteKernelForallValNatMemFinsetIicPartialTraj Finset.mem_Ioc not_le Finset.mem_Iic
lmarginalPartialTraj_le 📖	mathematical	Measurable ENNReal MeasurableSpace.pi ENNReal.measurableSpace	lmarginalPartialTraj	—	lmarginalPartialTraj.eq_1 Preorder.measurable_frestrictLe₂ partialTraj_le lintegral_deterministic' Measurable.comp measurable_updateFinset
lmarginalPartialTraj_mono 📖	mathematical	Pi.hasLe ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder	lmarginalPartialTraj	—	MeasureTheory.lintegral_mono
lmarginalPartialTraj_self 📖	mathematical	Measurable ENNReal MeasurableSpace.pi ENNReal.measurableSpace	lmarginalPartialTraj	—	eq_or_lt_of_le lmarginalPartialTraj_le le_rfl measurable_lmarginalPartialTraj Function.restrict_updateFinset Function.updateFinset_updateFinset_of_subset Finset.Iic_subset_Iic LT.lt.le lintegral_comp Measurable.fun_comp measurable_updateFinset partialTraj_comp_partialTraj
lmarginalPartialTraj_succ 📖	mathematical	ProbabilityTheory.IsSFiniteKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Measurable ENNReal ENNReal.measurableSpace	lmarginalPartialTraj MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike Preorder.frestrictLe Function.update	—	lmarginalPartialTraj.eq_1 partialTraj_succ_self lintegral_map measurable_IicProdIoc Measurable.fun_comp measurable_updateFinset lintegral_id_prod IsSFiniteKernel.map MeasurableEquiv.measurable Measurable.prodMk measurable_const measurable_id' Finset.mem_Ioc not_le Finset.mem_Iic
map_partialTraj_succ_self 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	map Finset.instMembership Preorder.toLE Finset.mem_Iic le_rfl partialTraj	—	Finset.mem_Iic le_rfl IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd partialTraj_succ_self map_comp_right measurable_IicProdIoc measurable_pi_apply Measurable.snd measurable_id' MeasurableEquiv.measurable snd_eq snd_prod instIsMarkovKernelId IsSFiniteKernel.map IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel MeasurableEquiv.symm_comp_self map_id
measurable_lmarginalPartialTraj 📖	mathematical	Measurable ENNReal MeasurableSpace.pi ENNReal.measurableSpace	lmarginalPartialTraj	—	Preorder.measurable_frestrictLe Measurable.lintegral_kernel_prod_left' IsSFiniteKernel.comap instIsSFiniteKernelForallValNatMemFinsetIicPartialTraj Measurable.comp Measurable.fun_comp measurable_pi_apply Measurable.fst measurable_id' Measurable.snd
partialTraj_comp_partialTraj 📖	mathematical	—	comp MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder partialTraj	—	Nat.le_induction partialTraj_self id_comp partialTraj_succ_eq_comp comp_assoc LE.le.trans
partialTraj_comp_partialTraj' 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	comp partialTraj	—	le_total partialTraj_comp_partialTraj Preorder.measurable_frestrictLe₂ partialTraj_le deterministic_comp_eq_map partialTraj_map_frestrictLe₂
partialTraj_comp_partialTraj'' 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	comp partialTraj	—	Preorder.measurable_frestrictLe₂ partialTraj_le deterministic_comp_eq_map partialTraj_map_frestrictLe₂
partialTraj_eq_prod 📖	mathematical	ProbabilityTheory.IsSFiniteKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	partialTraj map Prod.instMeasurableSpace Finset.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Nat.instLinearOrder prod id Finset.restrict₂ Finset.Ioc_subset_Iic_self IicProdIoc	—	Finset.Ioc_subset_Iic_self le_total Preorder.measurable_frestrictLe₂ partialTraj_le IicProdIoc_le map_comp_right Measurable.fst measurable_id' fst_eq Measurable.comp Finset.measurable_restrict₂ deterministic_map fst_prod IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelId isMarkovKernel_deterministic id_map Nat.le_induction ext partialTraj_self map_apply measurable_IicProdIoc prod_apply IicProdIoc_self MeasureTheory.Measure.fst.eq_1 MeasureTheory.Measure.fst_prod ProbabilityTheory.IsSFiniteKernel.sFinite ProbabilityTheory.IsMarkovKernel.is_probability_measure' LE.le.trans Finset.mem_Iic Finset.mem_Ioc not_le partialTraj_comp_partialTraj partialTraj_succ_self comp_map comap_map_comm comap_prod IsSFiniteKernel.map id_comap map_prod_eq isFiniteKernel_of_isFiniteKernel_snd IsZeroOrMarkovKernel.snd IsSFiniteKernel.comap Measurable.prodMap MeasurableEquiv.measurable Measurable.fun_comp measurable_IocProdIoc measurable_fst measurable_snd id_prod_eq prodAssoc_prod map_prod_map IsSFiniteKernel.prod map_id map_comp map_apply_eq_iff_map_symm_apply_eq instIsSFiniteKernelForallValNatMemFinsetIicPartialTraj MeasurableEquiv.coe_IicProdIoc MeasurableEquiv.symm_comp_self IicProdIoc_comp_restrict₂ deterministic_congr deterministic_comp_deterministic comp_deterministic_eq_comap
partialTraj_le 📖	mathematical	—	partialTraj deterministic MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Preorder.frestrictLe₂ Preorder.measurable_frestrictLe₂	—	Preorder.measurable_frestrictLe₂ partialTraj.eq_1
partialTraj_le_def 📖	mathematical	—	partialTraj Nat.leRec ProbabilityTheory.Kernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder id map Prod.instMeasurableSpace Finset.Ioc comp prod DFunLike.coe MeasurableEquiv EquivLike.toFunLike MeasurableEquiv.instEquivLike MeasurableEquiv.piSingleton IicProdIoc Nat.instLinearOrder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	eq_or_lt_of_le partialTraj_self Nat.leRec_self partialTraj.eq_1 not_le
partialTraj_map_frestrictLe₂ 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	map partialTraj Preorder.frestrictLe₂	—	Nat.le_induction map_id LE.le.trans Preorder.frestrictLe₂_comp_frestrictLe₂ map_comp_right Preorder.measurable_frestrictLe₂ partialTraj_succ_map_frestrictLe₂
partialTraj_map_frestrictLe₂_apply 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	MeasureTheory.Measure.map Preorder.frestrictLe₂ DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike partialTraj	—	map_apply Preorder.measurable_frestrictLe₂ partialTraj_map_frestrictLe₂
partialTraj_self 📖	mathematical	—	partialTraj id MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	—	le_rfl Preorder.measurable_frestrictLe₂ partialTraj_le
partialTraj_succ_eq_comp 📖	mathematical	—	partialTraj comp MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	—	partialTraj_succ_self map_comp partialTraj_succ_of_le
partialTraj_succ_map_frestrictLe₂ 📖	mathematical	ProbabilityTheory.IsMarkovKernel MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	map partialTraj Preorder.frestrictLe₂	—	le_or_gt IsMarkovKernel.map MeasurableEquiv.measurable partialTraj_succ_eq_comp map_comp partialTraj_succ_self map_comp_right measurable_IicProdIoc Preorder.measurable_frestrictLe₂ frestrictLe₂_comp_IicProdIoc fst_eq fst_prod IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelId id_comp partialTraj_le LT.lt.le Measurable.comp deterministic_map
partialTraj_succ_of_le 📖	mathematical	—	partialTraj map MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Prod.instMeasurableSpace Finset.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Nat.instLinearOrder comp prod id DFunLike.coe MeasurableEquiv EquivLike.toFunLike MeasurableEquiv.instEquivLike MeasurableEquiv.piSingleton IicProdIoc	—	partialTraj.eq_1 Nat.le_induction Nat.leRec_succ Nat.leRec_self comp_id partialTraj_self partialTraj_le_def
partialTraj_succ_self 📖	mathematical	—	partialTraj map MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder Prod.instMeasurableSpace Finset.Ioc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Nat.instLinearOrder prod id DFunLike.coe MeasurableEquiv EquivLike.toFunLike MeasurableEquiv.instEquivLike MeasurableEquiv.piSingleton IicProdIoc	—	partialTraj_succ_of_le le_rfl partialTraj_self comp_id
partialTraj_zero 📖	mathematical	—	partialTraj deterministic MeasurableSpace.pi Finset SetLike.instMembership Finset.instSetLike Finset.Iic Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Nat.instAddMonoid Preorder.frestrictLe₂ zero_le Nat.instCanonicallyOrderedAdd Preorder.measurable_frestrictLe₂	—	zero_le Nat.instCanonicallyOrderedAdd Preorder.measurable_frestrictLe₂ partialTraj_le

---

← Back to Index