Setoid associated to filter

Stream: Is there code for X?

[Adam Topaz]

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⟩

[Reid Barton]

See order.filter.germ

[Reid Barton]

also .filter_product

[Adam Topaz]

Ah nice. thanks.

[Adam Topaz]

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

[Adam Topaz]

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

[Reid Barton]

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

[Adam Topaz]

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

[Bryan Gin-ge Chen]

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

[Kenny Lau]

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

[Adam Topaz]

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

[Kevin Buzzard]

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

[Reid Barton]

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

[Yury G. Kudryashov]

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.

[Yury G. Kudryashov]

git grep -i is a good search tool.