Zulip Chat Archive

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"?

Adam Topaz (Oct 27 2020 at 13:30):

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 )

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

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: Dec 20 2023 at 11:08 UTC