Zulip Chat Archive
Stream: FLT-regular
Topic: Intervals in fin n
Riccardo Brasca (Dec 21 2021 at 19:46):
@Yaël Dillies Can you please have a look at the first four lemmas here? I am going to PR them, so it makes sense to add all the possible variations, and I don't want to waste time if they are not done correctly. What we really want is filter_lt_card and filter_gt_card. Thanks!
Notification Bot (Dec 21 2021 at 19:47):
Riccardo Brasca has marked this topic as resolved.
Notification Bot (Dec 21 2021 at 19:47):
Riccardo Brasca has marked this topic as unresolved.
Yaël Dillies (Dec 21 2021 at 19:48):
filter_lt_card and filter_gt_card are basically docs#finset.card_Iio and docs#finset.card_Ioi.
Yaël Dillies (Dec 21 2021 at 19:50):
The first two are worth having, but for fintype α, locally_finite_order α.
Yaël Dillies (Dec 21 2021 at 19:51):
They should go in data.finset.locally_finite. I can PR them if you prefer.
Riccardo Brasca (Dec 21 2021 at 19:53):
The reason why I use finset.filter is that I need docs#matrix.det_vandermonde, that is stated that way. Maybe it's better to modify it to use the interval notation?
Yaël Dillies (Dec 21 2021 at 19:53):
Oh yes, definitely!
Riccardo Brasca (Dec 21 2021 at 19:55):
Feel free to PR the modification if you want :sweat_smile:
Yaël Dillies (Dec 21 2021 at 19:57):
Oh sure! That will put me one PR further down my #RoadToBhavik :grinning_face_with_smiling_eyes:
Kevin Buzzard (Dec 21 2021 at 19:58):
Lol
Riccardo Brasca (Dec 21 2021 at 19:58):
This is going to break docs#algebra.discr_power_basis_eq_prod, but it should be enough to modify the statement accordingly
Riccardo Brasca (Dec 27 2021 at 12:15):
Mmh, docs#matrix.det_vandermonde works also for n = 0, and in that case we can't use docs#finset.Ioi since fin 0 has no top element. @Yaël Dillies do you see a workaround? Otherwise let's keep finset.filter.
Yaël Dillies (Dec 27 2021 at 12:16):
Hmm... unfortunately we don't have a typeclass saying "order_bot or empty". So I guess not.
Riccardo Brasca (Dec 27 2021 at 12:19):
No problem, I will add Ioi_eq_filter and friends.
Yaël Dillies (Dec 27 2021 at 12:36):
They should go the other way, as Ixx is preferred to filter.
Yakov Pechersky (Dec 27 2021 at 12:47):
@Yael, why is finset.Ioi defined via finset.Ioc and not finset.filter (> a) univ? That way you get the equiv to Ioc in order_top and it works elsewhere still.
Yaël Dillies (Dec 27 2021 at 13:11):
That's because they work over infinite types as well.
Yaël Dillies (Dec 27 2021 at 13:12):
Your proposal doesn't work for
Alex J. Best (Dec 27 2021 at 14:22):
Perhaps Ioi could take a typeclass argument locally_finite_order (with_top α) and be defined as Ioo x \top (but then pushed back down to α)? And then there would be instances of [fintype α] : locally_finite_order (with_top α) (coming from all finite order things being locally_finite) and [locally_finite_order α] [order_top α] : locally_finite_order (with_top α) ?
Yaël Dillies (Dec 27 2021 at 14:26):
Oh, that's actually pretty smart. However, you need more careful than that because we have docs#with_top.locally_finite_order
Yaël Dillies (Dec 27 2021 at 14:28):
Sorry, I mean that if we have [fintype α] [locally_finite_order α] [order_top α] then we get conflicting instances on with_top α. A safer bet would be [is_empty α] : locally_finite_order (with_top α) even though that sounds a bit stupid at first glance.
Yaël Dillies (Dec 27 2021 at 14:30):
This is because [is_empty α] [order_top α] will never be fulfilled.
Alex J. Best (Dec 27 2021 at 14:30):
But there are still other finite orders without tops that one might want to consider Ioi of though right?
Yaël Dillies (Dec 27 2021 at 14:31):
Yes, but those should assume locally_finite_order.
Yaël Dillies (Dec 27 2021 at 14:31):
It's data
Yaël Dillies (Dec 27 2021 at 14:32):
Of course, we could decide that we don't care about defeqness on fintypes and just go with [fintype α] : locally_finite_order α.
Alex J. Best (Dec 27 2021 at 14:34):
I think the instances I'm talking about are the same as yours though?
Yaël Dillies (Dec 27 2021 at 14:36):
The second one, yes. The first one, no.
Riccardo Brasca (Dec 21 2021 at 19:46):
@Yaël Dillies Can you please have a look at the first four lemmas here? I am going to PR them, so it makes sense to add all the possible variations, and I don't want to waste time if they are not done correctly. What we really want is filter_lt_card and filter_gt_card. Thanks!
Notification Bot (Dec 21 2021 at 19:47):
Riccardo Brasca has marked this topic as resolved.
Notification Bot (Dec 21 2021 at 19:47):
Riccardo Brasca has marked this topic as unresolved.
Yaël Dillies (Dec 21 2021 at 19:48):
filter_lt_card and filter_gt_card are basically docs#finset.card_Iio and docs#finset.card_Ioi.
Yaël Dillies (Dec 21 2021 at 19:50):
The first two are worth having, but for fintype α, locally_finite_order α.
Yaël Dillies (Dec 21 2021 at 19:51):
They should go in data.finset.locally_finite. I can PR them if you prefer.
Riccardo Brasca (Dec 21 2021 at 19:53):
The reason why I use finset.filter is that I need docs#matrix.det_vandermonde, that is stated that way. Maybe it's better to modify it to use the interval notation?
Yaël Dillies (Dec 21 2021 at 19:53):
Oh yes, definitely!
Riccardo Brasca (Dec 21 2021 at 19:55):
Feel free to PR the modification if you want :sweat_smile:
Yaël Dillies (Dec 21 2021 at 19:57):
Oh sure! That will put me one PR further down my #RoadToBhavik :grinning_face_with_smiling_eyes:
Kevin Buzzard (Dec 21 2021 at 19:58):
Lol
Riccardo Brasca (Dec 21 2021 at 19:58):
This is going to break docs#algebra.discr_power_basis_eq_prod, but it should be enough to modify the statement accordingly
Riccardo Brasca (Dec 27 2021 at 12:15):
Mmh, docs#matrix.det_vandermonde works also for n = 0, and in that case we can't use docs#finset.Ioi since fin 0 has no top element. @Yaël Dillies do you see a workaround? Otherwise let's keep finset.filter.
Yaël Dillies (Dec 27 2021 at 12:16):
Hmm... unfortunately we don't have a typeclass saying "order_bot or empty". So I guess not.
Riccardo Brasca (Dec 27 2021 at 12:19):
No problem, I will add Ioi_eq_filter and friends.
Yaël Dillies (Dec 27 2021 at 12:36):
They should go the other way, as Ixx is preferred to filter.
Yakov Pechersky (Dec 27 2021 at 12:47):
@Yael, why is finset.Ioi defined via finset.Ioc and not finset.filter (> a) univ? That way you get the equiv to Ioc in order_top and it works elsewhere still.
Yaël Dillies (Dec 27 2021 at 13:11):
That's because they work over infinite types as well.
Yaël Dillies (Dec 27 2021 at 13:12):
Your proposal doesn't work for
Alex J. Best (Dec 27 2021 at 14:22):
Perhaps Ioi could take a typeclass argument locally_finite_order (with_top α) and be defined as Ioo x \top (but then pushed back down to α)? And then there would be instances of [fintype α] : locally_finite_order (with_top α) (coming from all finite order things being locally_finite) and [locally_finite_order α] [order_top α] : locally_finite_order (with_top α) ?
Yaël Dillies (Dec 27 2021 at 14:26):
Oh, that's actually pretty smart. However, you need more careful than that because we have docs#with_top.locally_finite_order
Yaël Dillies (Dec 27 2021 at 14:28):
Sorry, I mean that if we have [fintype α] [locally_finite_order α] [order_top α] then we get conflicting instances on with_top α. A safer bet would be [is_empty α] : locally_finite_order (with_top α) even though that sounds a bit stupid at first glance.
Yaël Dillies (Dec 27 2021 at 14:30):
This is because [is_empty α] [order_top α] will never be fulfilled.
Alex J. Best (Dec 27 2021 at 14:30):
But there are still other finite orders without tops that one might want to consider Ioi of though right?
Yaël Dillies (Dec 27 2021 at 14:31):
Yes, but those should assume locally_finite_order.
Yaël Dillies (Dec 27 2021 at 14:31):
It's data
Yaël Dillies (Dec 27 2021 at 14:32):
Of course, we could decide that we don't care about defeqness on fintypes and just go with [fintype α] : locally_finite_order α.
Alex J. Best (Dec 27 2021 at 14:34):
I think the instances I'm talking about are the same as yours though?
Yaël Dillies (Dec 27 2021 at 14:36):
The second one, yes. The first one, no.
Last updated: Dec 20 2023 at 11:08 UTC