Zulip Chat Archive

Stream: Is there code for X?

Topic: Setoid associated to filter


view this post on Zulip Adam Topaz (Sep 10 2020 at 15:34):

Does mathlib already have something like the following?

import order.filter.basic
variables {B : Type*} (T : B  Type*) (F : filter B)
example : setoid (Π b, T b) := ⟨λ f g,  b in F, f b = g b, sorry

view this post on Zulip Reid Barton (Sep 10 2020 at 15:34):

See order.filter.germ

view this post on Zulip Reid Barton (Sep 10 2020 at 15:35):

also .filter_product

view this post on Zulip Adam Topaz (Sep 10 2020 at 15:35):

Ah nice. thanks.

view this post on Zulip Adam Topaz (Sep 10 2020 at 15:36):

Oh good mathlib already has ultraproducts. that's what I needed anyway :)

view this post on Zulip Adam Topaz (Sep 10 2020 at 15:37):

Why isn't order.​filter.​filter_product called order.​filter.​ultraproduct ?

view this post on Zulip Reid Barton (Sep 10 2020 at 15:38):

I was going to say I think filterproduct is another name for ultraproduct, but filterproduct doesn't seem to appear anywhere in the file, so ... yeah

view this post on Zulip Adam Topaz (Sep 10 2020 at 15:45):

This is what I tried first...
Screenshot_2020-09-10-mathlib-docs-index.png

view this post on Zulip Bryan Gin-ge Chen (Sep 10 2020 at 15:46):

Looks like a doc / renaming PR is in order...

view this post on Zulip Kenny Lau (Sep 10 2020 at 16:29):

@Adam Topaz https://github.com/leanprover-community/mathlib/search?q=ultraproduct&unscoped_q=ultraproduct

view this post on Zulip Adam Topaz (Sep 10 2020 at 17:23):

Kenny Lau said:

Adam Topaz https://github.com/leanprover-community/mathlib/search?q=ultraproduct&unscoped_q=ultraproduct

Thanks. I never remember to try github's search or git grep

view this post on Zulip Kevin Buzzard (Sep 10 2020 at 17:31):

The API search should work for this. Git grep is a hack which users aren't supposed to need

view this post on Zulip Reid Barton (Sep 10 2020 at 17:37):

The module docstring does already contain the words Ultraproduct, ultraproduct and ultraproducts

view this post on Zulip Yury G. Kudryashov (Sep 14 2020 at 20:33):

First @Abhimanyu Pallavi Sudhir defined ultraproducts for hyperreals. He used names bigly_equal and filter_product and the header said: "Filterproducts" (ultraproducts on general filters), ultraproducts.
Then I renamed filter_product to germ leaving in src/order/filter/filter_product theorems that assume is_ultrafilter. Feel free to rename this file to ultraproduct but please leave filter.germ named this way because this name is much more common in standard analysis.

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

git grep -i is a good search tool.


Last updated: May 16 2021 at 05:21 UTC