Skip to content
Snippets Groups Projects
Commit 02b2b2ac authored by François Clément's avatar François Clément
Browse files

(sigma_algebra.v) Add measurable_seq. 

(measurable_fun.v) Add incr_fun_seq, measurable_fun_seq_Rbar,
  Mplus, Mplus_finite, Mplus_seq, Mplus_ext, Mplus_seq_ext,
  many Mplus_* lemmas.

(simple_fun.v) Add SFplus_Mplus.

And use them!
parent 6b945799
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 777 additions and 699 deletions
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment