## Stream: general

### Topic: Name?

#### Yury G. Kudryashov (Oct 27 2020 at 13:07):

What is the correct name for the typeclass "all sets are measurable"?

Discrete?

#### Kevin Buzzard (Oct 27 2020 at 14:23):

There's a model of ZF where AC fails and all subsets of the reals are measurable, and the reals aren't discrete :-/

#### Mario Carneiro (Oct 27 2020 at 14:24):

vitali_averse

#### Kevin Buzzard (Oct 27 2020 at 14:24):

In the presence of AC is this equivalent to discrete? Does the counting measure on the rationals with its usual topology have the property that every subset is measurable?

#### Mario Carneiro (Oct 27 2020 at 14:26):

For a measurable space, this is just M = \top. There are lots of non-top measurable spaces, like borel sets

#### Mario Carneiro (Oct 27 2020 at 14:27):

if you want a measure space, then there are again lots of examples where the measure is trivial in some sense, like the counting measure

#### Mario Carneiro (Oct 27 2020 at 14:27):

every subset of the reals with counting measure is measurable

#### Mario Carneiro (Oct 27 2020 at 14:29):

Vitali's theorem says that lebesgue measure is not defined on \top

#### Mario Carneiro (Oct 27 2020 at 14:31):

and it applies more generally to nontrivial translation-invariant measures on the reals

#### Yury G. Kudryashov (Oct 27 2020 at 14:34):

Yes, I'm looking for a name for the typeclass _inst_1 = \top

#### Yury G. Kudryashov (Oct 27 2020 at 14:35):

Like we have a name for "topology = \bot"

#### Adam Topaz (Oct 27 2020 at 14:43):

I don't see the problem with a name involving "discrete" in some way. E.g. the discrete $\sigma$-algebra is a name for the largest $\sigma$-algebra (at least according to wikipedia: https://en.wikipedia.org/wiki/%CE%A3-algebra#Particular_cases_and_examples )

OK, thanks

#### Yury G. Kudryashov (Mar 16 2021 at 22:33):

How would you call this operation?

variables {α : Type*}

def new_op (op : α → α → α) : list α → list α
| [] := []
| [a] := [a]
| (a :: b :: l) := a :: (op a b) :: new_op (b :: l)


#### Yakov Pechersky (Mar 16 2021 at 22:34):

cum_scanl?

#### Yury G. Kudryashov (Mar 16 2021 at 22:39):

It's not scanl. It's a combination of zip/map₂ and interleave

#### Yury G. Kudryashov (Mar 16 2021 at 22:39):

(not exactly because I leave the last element of the original list)

#### Yakov Pechersky (Mar 16 2021 at 22:40):

isn't it like a modified scanl (zip l l.tail)?

#### Yury G. Kudryashov (Mar 16 2021 at 22:43):

scanl f a [b, c] produces [a, f a b, f (f a b) c]

#### Yury G. Kudryashov (Mar 16 2021 at 22:43):

E.g., scanl (+) 0 [1, 2, 3] = [0, 1, 3, 6]

#### Yury G. Kudryashov (Mar 16 2021 at 22:43):

My operation works as new_op (+) [a, b, c] = [a, a + b, b, b + c, c]

#### Anne Baanen (Mar 17 2021 at 08:47):

How about intersperse_map or intersperse_zip?

#### Eric Wieser (Mar 17 2021 at 08:54):

Do we have a definition that sends foo (+) [a, b, c, d] to [a + b, b + c, c + d]?

#### Bhavik Mehta (Mar 17 2021 at 12:46):

foo o l = zipWith o l l.tail should do this

Last updated: May 13 2021 at 23:16 UTC