| Wed, 07 Oct 2015 17:11:16 +0200 |
hoelzl |
cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 20:20:16 +0200 |
wenzelm |
renamed method "goals" to "goal_cases" to emphasize its meaning;
|
file |
diff |
annotate
|
| Thu, 23 Jul 2015 16:40:47 +0200 |
hoelzl |
Measures form a CCPO
|
file |
diff |
annotate
|
| Thu, 16 Jul 2015 10:48:20 +0200 |
hoelzl |
move disjoint sets to their own theory
|
file |
diff |
annotate
|
| Mon, 13 Jul 2015 14:40:16 +0200 |
hoelzl |
add emeasure_add_AE
|
file |
diff |
annotate
|
| Mon, 13 Jul 2015 14:39:50 +0200 |
hoelzl |
stronger induction assumption in lfp_transfer and emeasure_lfp
|
file |
diff |
annotate
|
| Fri, 03 Jul 2015 08:26:34 +0200 |
hoelzl |
add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
|
file |
diff |
annotate
|
| Fri, 26 Jun 2015 10:20:33 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 25 Jun 2015 23:33:47 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 04 May 2015 17:35:31 +0200 |
hoelzl |
rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
|
file |
diff |
annotate
|
| Wed, 22 Apr 2015 12:43:06 +0100 |
paulson |
fixes for limits
|
file |
diff |
annotate
|
| Tue, 21 Apr 2015 17:19:00 +0100 |
paulson |
New material, mostly about limits. Consolidation.
|
file |
diff |
annotate
|
| Tue, 14 Apr 2015 14:11:01 +0200 |
Andreas Lochbihler |
add lemmas about restrict_space
|
file |
diff |
annotate
|
| Thu, 05 Mar 2015 11:11:42 +0100 |
hoelzl |
fix import path
|
file |
diff |
annotate
|
| Thu, 22 Jan 2015 14:51:08 +0100 |
hoelzl |
import general thms from Density_Compiler
|
file |
diff |
annotate
|