Documentation Verification Report

Update

📁 Source: Mathlib/Data/Finset/Update.lean

Statistics

Metric	Count
Definitions `updateFinset`	1
Theorems `update`, `updateFinset`, `restrict_updateFinset`, `restrict_updateFinset_of_subset`, `updateFinset_congr`, `updateFinset_def`, `updateFinset_empty`, `updateFinset_restrict`, `updateFinset_singleton`, `updateFinset_univ`, `updateFinset_univ_apply`, `updateFinset_updateFinset`, `updateFinset_updateFinset_of_subset`, `update_eq_updateFinset`, `update_updateFinset`	15
Total	16

DependsOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`update` 📖	mathematical	`DependsOn` `SetLike.coe` `Finset` `Finset.instSetLike`	`Function.update` `Finset.erase`	—	`Function.update_eq_updateFinset` `Finset.erase_eq` `Finset.coe_sdiff` `updateFinset`
`updateFinset` 📖	mathematical	`DependsOn`	`Function.updateFinset` `Set` `Set.instSDiff` `SetLike.coe` `Finset` `Finset.instSetLike`	—	—

Function

Definitions

Name	Category	Theorems
`updateFinset` 📖	CompOp	27 math math: `update_eq_updateFinset`, `ProbabilityTheory.Kernel.condExp_traj'`, `restrict_updateFinset`, `MeasureTheory.integral_infinitePi_of_piFinset`, `ProbabilityTheory.Kernel.traj_map_updateFinset`, `updateFinset_congr`, `DependsOn.updateFinset`, `update_updateFinset`, `updateFinset_singleton`, `Preorder.frestrictLe_updateFinset`, `ProbabilityTheory.Kernel.lintegral_traj`, `measurable_updateFinset`, `updateFinset_updateFinset`, `Preorder.frestrictLe_updateFinset_of_le`, `measurable_updateFinset_left`, `updateFinset_restrict`, `updateFinset_univ_apply`, `measurable_updateFinset'`, `updateFinset_empty`, `restrict_updateFinset_of_subset`, `updateFinset_univ`, `ProbabilityTheory.Kernel.integral_traj`, `updateFinset_def`, `Preorder.updateFinset_frestrictLe`, `ProbabilityTheory.Kernel.lintegral_traj₀`, `updateFinset_updateFinset_of_subset`, `ProbabilityTheory.Kernel.lmarginalPartialTraj_eq_lintegral_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`restrict_updateFinset` 📖	mathematical	—	`Finset.restrict` `updateFinset`	—	`subset_rfl` `Finset.instReflSubset` `restrict_updateFinset_of_subset`
`restrict_updateFinset_of_subset` 📖	mathematical	`Finset` `Finset.instHasSubset`	`Finset.restrict` `updateFinset` `Finset.restrict₂`	—	—
`updateFinset_congr` 📖	mathematical	—	`updateFinset` `Finset` `SetLike.instMembership` `Finset.instSetLike`	—	—
`updateFinset_def` 📖	mathematical	—	`updateFinset` `Finset` `Finset.instMembership` `Finset.decidableMem` `SetLike.instMembership` `Finset.instSetLike`	—	—
`updateFinset_empty` 📖	mathematical	—	`updateFinset` `Finset` `Finset.instEmptyCollection`	—	—
`updateFinset_restrict` 📖	mathematical	—	`updateFinset` `Finset.restrict`	—	—
`updateFinset_singleton` 📖	mathematical	—	`updateFinset` `Finset` `Finset.instSingleton` `update` `SetLike.instMembership` `Finset.instSetLike` `Finset.mem_singleton_self`	—	`Finset.mem_singleton_self` `update_self` `update_of_ne`
`updateFinset_univ` 📖	mathematical	—	`updateFinset` `Finset.univ` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.mem_univ`	—	`Finset.mem_univ`
`updateFinset_univ_apply` 📖	mathematical	—	`updateFinset` `Finset.univ` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.mem_univ`	—	`Finset.mem_univ`
`updateFinset_updateFinset` 📖	mathematical	`Disjoint` `Finset` `Finset.partialOrder` `Finset.instOrderBot`	`updateFinset` `Finset.instUnion` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.piFinsetUnion`	—	`Finset.disjoint_left` `Equiv.piCongrLeft_sumInl` `Equiv.piCongrLeft_sumInr`
`updateFinset_updateFinset_of_subset` 📖	mathematical	`Finset` `Finset.instHasSubset`	`updateFinset`	—	—
`update_eq_updateFinset` 📖	mathematical	—	`update` `updateFinset` `Finset` `Finset.instSingleton` `uniqueElim` `SetLike.instMembership` `Finset.instSetLike` `Finset.instUniqueSubtypeMemSingleton`	—	`update_self` `uniqueElim_default` `update_of_ne`
`update_updateFinset` 📖	mathematical	`Finset` `Finset.instMembership`	`update` `updateFinset` `Finset.instUnion` `Finset.instSingleton` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.piFinsetUnion` `Disjoint` `Finset.partialOrder` `Finset.instOrderBot` `Finset.disjoint_singleton_right` `uniqueElim` `SetLike.instMembership` `Finset.instSetLike` `Finset.instUniqueSubtypeMemSingleton`	—	`Finset.disjoint_singleton_right` `update_eq_updateFinset` `updateFinset_updateFinset`

---

← Back to Index