## Stream: new members

### Topic: A picture of [0,oo]

#### Lars Ericson (Dec 11 2020 at 05:20):

Just for fun:
Screenshot-from-2020-12-11-00-19-25.png

#### Kenny Lau (Dec 11 2020 at 06:04):

how did you do that?

#### Lars Ericson (Dec 11 2020 at 14:24):

In Python in a Jupyter notebook, by hand, after picking out all the definitions, like this:

from graphviz import Digraph
def show(e):
g = Digraph(comment='Grundbegriffe')
g.attr(shape='box')
for a,b in e:
g.node(a, shape='box')
g.node(b, shape='box')
g.edge(a,b)
return g

show([('probability_space', 'Steinhaus'),
('P_I01', 'Steinhaus'),
('measure_space', 'probability_space'),
('measure', 'probability_measure'),
('measure', 'measure_space'),
('probability_measure', 'probability_space'),
('probability_measure', 'P_I01'),
('I01', 'P_I01'),
('set', 'I01'),
('ℝ', 'I01')
])


which gives

The notebook is here.

I am trying to teach some friends about approximation of solution to stochastic processes using an ancient book written in a dead language. Because I don't really know anything, in particular, I don't know enough what is trivial window-dressing that I should take for granted, I am stuck on an irrelevant concept on page 3, and I thought Lean might help me clear up my thinking:

Screenshot-from-2020-12-11-09-21-25.png

Last updated: May 15 2021 at 22:14 UTC