Finish some proofs.
Comment unused admitted results (and rename dmit -> glop). Subset_system: Add and prove Gen_Prod_Gen_Product.
Showing
- Lebesgue/Subset.v 4 additions, 7 deletionsLebesgue/Subset.v
- Lebesgue/Subset_system.v 20 additions, 5 deletionsLebesgue/Subset_system.v
- Lebesgue/Subset_system_base.v 10 additions, 12 deletionsLebesgue/Subset_system_base.v
- Lebesgue/Tonelli.v 24 additions, 28 deletionsLebesgue/Tonelli.v
- Lebesgue/Topology.v 4 additions, 2 deletionsLebesgue/Topology.v
- Lebesgue/UniformSpace_compl.v 3 additions, 1 deletionLebesgue/UniformSpace_compl.v
- Lebesgue/measurable.v 3 additions, 1 deletionLebesgue/measurable.v
- Lebesgue/measurable_Rbar.v 5 additions, 5 deletionsLebesgue/measurable_Rbar.v
- Lebesgue/measurable_fun_new.v 1 addition, 1 deletionLebesgue/measurable_fun_new.v
Loading
Please register or sign in to comment