Zulip Chat Archive

Stream: general

Topic: Name?


view this post on Zulip Yury G. Kudryashov (Oct 27 2020 at 13:07):

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

view this post on Zulip Adam Topaz (Oct 27 2020 at 13:30):

Discrete?

view this post on Zulip 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 :-/

view this post on Zulip Mario Carneiro (Oct 27 2020 at 14:24):

vitali_averse

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 27 2020 at 14:27):

every subset of the reals with counting measure is measurable

view this post on Zulip Mario Carneiro (Oct 27 2020 at 14:29):

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

view this post on Zulip Mario Carneiro (Oct 27 2020 at 14:31):

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

view this post on Zulip Yury G. Kudryashov (Oct 27 2020 at 14:34):

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

view this post on Zulip Yury G. Kudryashov (Oct 27 2020 at 14:35):

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

view this post on Zulip 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 )

view this post on Zulip Yury G. Kudryashov (Oct 27 2020 at 14:44):

OK, thanks

view this post on Zulip 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)

view this post on Zulip Yakov Pechersky (Mar 16 2021 at 22:34):

cum_scanl?

view this post on Zulip Yury G. Kudryashov (Mar 16 2021 at 22:39):

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

view this post on Zulip Yury G. Kudryashov (Mar 16 2021 at 22:39):

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

view this post on Zulip Yakov Pechersky (Mar 16 2021 at 22:40):

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

view this post on Zulip Yury G. Kudryashov (Mar 16 2021 at 22:43):

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

view this post on Zulip Yury G. Kudryashov (Mar 16 2021 at 22:43):

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

view this post on Zulip 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]

view this post on Zulip Anne Baanen (Mar 17 2021 at 08:47):

How about intersperse_map or intersperse_zip?

view this post on Zulip 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]?

view this post on Zulip 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