# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Filter golf

#### Heather Macbeth (Feb 22 2021 at 17:52):

Is there a slick way of proving this fact about filters?

```
example {α β γ δ} [topological_space γ] [topological_space δ] {f : α → γ} {g : β → δ}
(hf : tendsto f cofinite (cocompact _)) (hg : tendsto g cofinite (cocompact _)) :
tendsto (λ x : α × β, (f x.1, g x.2)) cofinite (cocompact _) :=
```

At the moment I have a long proof, but perhaps I am unpacking things that don't need to be unpacked.

```
import topology.subset_properties
open filter
lemma filter.tendsto.finite_preimage_compact {α : Type*} {β : Type*} [topological_space β]
{f : α → β} (hf : tendsto f cofinite (cocompact _)) {s : set β} (hs : is_compact s) :
set.finite (f ⁻¹' s) :=
begin
rw [tendsto_def] at hf,
have := hf sᶜ,
rw mem_cofinite at this,
convert this _,
{ simp },
rw mem_cocompact,
refine ⟨s, hs, rfl.subset⟩
end
example {α β γ δ} [topological_space γ] [topological_space δ] {f : α → γ} {g : β → δ}
(hf : tendsto f cofinite (cocompact _)) (hg : tendsto g cofinite (cocompact _)) :
tendsto (λ x : α × β, (f x.1, g x.2)) cofinite (cocompact _) :=
begin
simp only [tendsto_def, mem_cofinite, mem_cocompact'],
rintros s ⟨t, ht, hts⟩,
let t₁ : set γ := prod.fst '' t,
let t₂ : set δ := prod.snd '' t,
have ht₁ : is_compact t₁ := ht.image continuous_fst,
have ht₂ : is_compact t₂ := ht.image continuous_snd,
have hft : (f ⁻¹' t₁).finite := hf.finite_preimage_compact ht₁,
have hgt : (g ⁻¹' t₂).finite := hg.finite_preimage_compact ht₂,
refine (hft.prod hgt).subset _,
have : (λ x : α × β, (f x.1, g x.2)) ⁻¹' (t₁.prod t₂) = (f ⁻¹' t₁).prod (g ⁻¹' t₂),
{ ext,
simp },
rw ← this,
rw ← set.preimage_compl,
have ht' : t ⊆ t₁.prod t₂,
{ intros x hx,
exact ⟨⟨x, hx, rfl⟩, ⟨x, hx, rfl⟩⟩ },
refine set.preimage_mono (set.subset.trans hts ht'),
end
```

#### Kevin Buzzard (Feb 22 2021 at 18:20):

Nice question! I was wondering whether some `filter.prod`

trick could help, but it seems to me that the product of the cofinite filters on alpha and beta is not the cofinite filter on alpha x beta.

One thing I noticed when thinking about filters over the last week or so is that there's this dual concept of an ideal. Just like in topological spaces where it's equivalent to carry around the open sets or the closed sets, in a parallel universe the fundamental concept turned out not to be a filter but the ideal of sets whose complements were in the filter. So you get the finite ideal, the subset-of-compact ideal etc, and the axioms are just the duals of the filter axioms -- empty set is in the ideal, shrinking an element of the ideal gives you something in the ideal, and union of two things in the ideal is in the ideal. I would imagine that there's a product of ideals, and the product of two finite ideals is the finite ideal on the product, but somehow the fact that (a + b) * (c + d) isn't ac+bd means that this doesn't translate into the product of two cofinite filters being the cofinite filter.

#### Kevin Buzzard (Feb 22 2021 at 18:21):

I guess the reason filters caught on rather than ideals is that the neighbourhood filter translates into the ideal of subsets whose closure does not contain x, which has a "not" in so it's somehow an indication that you're doing something the wrong way around.

#### Adam Topaz (Feb 22 2021 at 18:22):

They're not the same filter, but they're comparable.

#### Kevin Buzzard (Feb 22 2021 at 18:25):

The reason I mention all this is that your proof is somehow ideal-theoretic. You're trying to prove the preimage of a cocompact set is cofinite, and this is the same as proving that the preimage of a subset-of-a-compact-set is finite. But any subset-of-a-compact-set is a subset of a product of subsets-of-a-compact-set (consider projections), and a product of finite sets is finite, so done. I know you know all this, I'm just noting that because we have all this machinery for filters and perhaps less machinery for ideals you're having to turn everything around manually.

#### Johan Commelin (Feb 22 2021 at 18:27):

Note that there recently was a PR about such ideals: #5937

#### Heather Macbeth (Feb 22 2021 at 18:36):

Adam Topaz said:

They're not the same filter, but they're comparable.

@Adam Topaz This comment refers to the relationship between `(cofinite : filter (α × β))`

and `(cofinite : filter α).prod (cofinite : filter β)`

?

#### Kevin Buzzard (Feb 22 2021 at 18:37):

Presumably comparable means one is < the other?

#### Adam Topaz (Feb 22 2021 at 18:39):

Yeah exactly.

#### Heather Macbeth (Feb 22 2021 at 18:39):

I see. But then presumably the same inequality holds for the relationship between `cocompact (α × β)`

and `(cocompact α).prod (cocompact β)`

, so it doesn't help us (one inequality goes the helpful direction, one the unhelpful direction)?

#### Adam Topaz (Feb 22 2021 at 18:39):

Hmm.... yeah you're probably right

#### Kevin Buzzard (Feb 22 2021 at 18:39):

Right, that's my gut instinct too

#### Kevin Buzzard (Feb 22 2021 at 18:40):

But with the ideals it might work perfectly

#### Kevin Buzzard (Feb 22 2021 at 18:40):

I think the filter prod is something like the meet of two pulled back ideals and we want the join,

#### Kevin Buzzard (Feb 22 2021 at 18:41):

Or possibly vice versa

#### Heather Macbeth (Feb 22 2021 at 18:41):

Kevin Buzzard said:

I would imagine that there's a product of ideals, and the product of two finite ideals is the finite ideal on the product, but somehow the fact that (a + b) * (c + d) isn't ac+bd means that this doesn't translate into the product of two cofinite filters being the cofinite filter.

It'd be nice to have a name and API for this operation on filters, whatever it is!

#### Kevin Buzzard (Feb 22 2021 at 18:49):

```
protected def coprod (f : filter α) (g : filter β) : filter (α × β) :=
f.comap prod.fst ⊔ g.comap prod.snd
```

? I've got no idea if `filter.coprod`

is a silly name for it.

#### Heather Macbeth (Feb 22 2021 at 19:06):

Ah, this is great! I can now prove

```
example : (cofinite : filter α).coprod (cofinite : filter β) = cofinite :=
```

#### Kevin Buzzard (Feb 22 2021 at 19:07):

Me too! So at least the construction isn't completely degenerate :-) Here's my effort:

```
import order.filter.cofinite
namespace filter
variables {α β : Type*}
protected def coprod (f : filter α) (g : filter β) : filter (α × β) :=
f.comap prod.fst ⊔ g.comap prod.snd
example (f : α → β) (S : set β) : f ⁻¹' Sᶜ = (f ⁻¹' S)ᶜ := set.preimage_compl
open set
example : filter.coprod (cofinite : filter α) (cofinite : filter β) = cofinite :=
begin
ext S,
unfold filter.coprod,
simp only [exists_prop, mem_comap_sets, mem_sup_sets, mem_cofinite] at *,
split,
{ rintro ⟨⟨A, hAf, hAS⟩, B, hBf, hBS⟩,
rw [← compl_subset_compl, ← preimage_compl] at hAS hBS,
let ABc := set.prod Aᶜ Bᶜ,
have hS : Sᶜ ⊆ ABc := subset_inter hAS hBS,
exact (finite.prod hAf hBf).subset hS,
},
{ intro hS,
split,
{ use (prod.fst '' Sᶜ)ᶜ,
rw compl_compl,
use hS.image prod.fst,
rw [preimage_compl, compl_subset_comm],
exact subset_preimage_image prod.fst Sᶜ },
{ use (prod.snd '' Sᶜ)ᶜ,
rw compl_compl,
use hS.image prod.snd,
rw [preimage_compl, compl_subset_comm],
exact subset_preimage_image prod.snd Sᶜ } },
end
end filter
```

#### Heather Macbeth (Feb 22 2021 at 19:08):

Presumably one also wants a lemma

```
example {α β γ δ} (a : filter α) (b : filter β) (c : filter γ) (d : filter δ) {f : α → γ} {g : β → δ}
(hf : tendsto f a c) (hg : tendsto g b d) :
tendsto (λ x : α × β, (f x.1, g x.2)) (a.coprod b) (c.coprod d) :=
```

#### Kevin Buzzard (Feb 22 2021 at 19:08):

I was rather hoping that `finish`

could take over at some point but I never managed to get it to :-(

#### Heather Macbeth (Feb 22 2021 at 19:08):

And then some category theorist should tell us whether we're allowed to call it a coproduct :)

#### Kevin Buzzard (Feb 22 2021 at 19:09):

So of course now the question is whether there is some kind of useful `tendsto.coprod`

#### Heather Macbeth (Feb 22 2021 at 19:09):

Heather Macbeth said:

Presumably one also wants a lemma

`example {α β γ δ} (a : filter α) (b : filter β) (c : filter γ) (d : filter δ) {f : α → γ} {g : β → δ} (hf : tendsto f a c) (hg : tendsto g b d) : tendsto (λ x : α × β, (f x.1, g x.2)) (a.coprod b) (c.coprod d) :=`

Yes, this, right?

#### Kevin Buzzard (Feb 22 2021 at 19:10):

So coproduct of cofinite will be cofinite, for basically the same reasons?

#### Heather Macbeth (Feb 22 2021 at 19:10):

You mean cocompact, right? I suspect so ....

#### Kevin Buzzard (Feb 22 2021 at 19:11):

Yes, sorry to add the confusion! cocompact.

#### Adam Topaz (Feb 22 2021 at 19:11):

Heather Macbeth said:

And then some category theorist should tell us whether we're allowed to call it a coproduct :)

If this is the coproduct in the category given by the lattice stucture, then sure! (looks like it is!)

#### Kevin Buzzard (Feb 22 2021 at 19:11):

The thing is that this "product of filters" isn't some internal product, it's a map `filter X x filter Y -> filter (X x Y)`

#### Heather Macbeth (Feb 22 2021 at 19:12):

(I need to go teach, see you in a bit)

#### Kevin Buzzard (Feb 22 2021 at 19:12):

For all I know, filter.coprod should go to `filter X \coprod Y`

or whatever

#### Adam Topaz (Feb 22 2021 at 19:12):

oh maybe it's not a good name then...

#### Kevin Buzzard (Feb 22 2021 at 19:26):

Heather Macbeth said:

Presumably one also wants a lemma

`example {α β γ δ} (a : filter α) (b : filter β) (c : filter γ) (d : filter δ) {f : α → γ} {g : β → δ} (hf : tendsto f a c) (hg : tendsto g b d) : tendsto (λ x : α × β, (f x.1, g x.2)) (a.coprod b) (c.coprod d) :=`

It's true :D

#### Kevin Buzzard (Feb 22 2021 at 19:29):

```
import order.filter.cofinite
namespace filter
variables {α β : Type*}
-- this corresponds to `ideal.prod`, where an ideal on a type X is
-- a set of subsets of X such that the complements of these sets
-- are a filter.
protected def coprod (f : filter α) (g : filter β) : filter (α × β) :=
f.comap prod.fst ⊔ g.comap prod.snd
open set
example : filter.coprod (cofinite : filter α) (cofinite : filter β) = cofinite :=
begin
ext S,
unfold filter.coprod,
simp only [exists_prop, mem_comap_sets, mem_sup_sets, mem_cofinite] at *,
split,
{ rintro ⟨⟨A, hAf, hAS⟩, B, hBf, hBS⟩,
rw [← compl_subset_compl, ← preimage_compl] at hAS hBS,
let ABc := set.prod Aᶜ Bᶜ,
have hS : Sᶜ ⊆ ABc := subset_inter hAS hBS,
exact (finite.prod hAf hBf).subset hS,
},
{ intro hS,
split,
{ use (prod.fst '' Sᶜ)ᶜ,
rw compl_compl,
use hS.image prod.fst,
rw [preimage_compl, compl_subset_comm],
exact subset_preimage_image prod.fst Sᶜ },
{ use (prod.snd '' Sᶜ)ᶜ,
rw compl_compl,
use hS.image prod.snd,
rw [preimage_compl, compl_subset_comm],
exact subset_preimage_image prod.snd Sᶜ } },
end
example {α β γ δ} (a : filter α) (b : filter β) (c : filter γ) (d : filter δ) {f : α → γ} {g : β → δ}
(hf : tendsto f a c) (hg : tendsto g b d) :
tendsto (λ x : α × β, (f x.1, g x.2)) (a.coprod b) (c.coprod d) :=
begin
rw tendsto_def,
intros s hs,
unfold filter.coprod at hs,
simp only [exists_prop, mem_comap_sets, mem_sup_sets] at hs,
rcases hs with ⟨⟨C, hCc, hCs⟩, ⟨D, hDd, hDs⟩⟩,
unfold filter.coprod,
simp only [exists_prop, mem_comap_sets, mem_sup_sets],
split,
{ rw tendsto_def at hf,
specialize hf C hCc,
use [f ⁻¹' C, hf],
rintro ⟨aa,bb⟩ haaC,
apply hCs,
exact haaC },
{ rw tendsto_def at hg,
specialize hg D hDd,
use [g ⁻¹' D, hg],
rintro ⟨aa,bb⟩ hbbD,
apply hDs,
exact hbbD },
end
end filter
```

#### Kevin Buzzard (Feb 22 2021 at 19:41):

About two weeks ago I would have ignored this question because I didn't know what a filter was. It was preparing last week's workshop and my current work on this week's workshop which meant that I was no longer scared of them. The way I'm thinking about filters now is that they are some kind of weird generalisation of subsets. Filters are a lattice containing the lattice of subsets (thought of as principal filters) as a sublattice, and given a filter F you can ask which subsets S have the property that F <= S. The fundamental fact about filters is that this set S of subsets determines the filter, and indeed F.sets is precisely these subsets. What about the subsets contained in F? For some reason these give far less information. This asymmetry is fixed if you model a filter by ideals; then you get some other model of a "fuzzy set" which is determined by the subsets it contains but not by the ones it's contained in. Given a subset you get a filter, the principal filter, and conversely given a filter you can just take the intersection of the subsets it is contained in and get some kind of "best approximation subset" of a filter. I am surprised that this isn't some fundamental construction, it seems to be some kind of standard adjoint functor / galois insertion thing but I couldn't find it in order.filter.basic .

That was what I learnt last week. This week I've been thinking about `tendsto`

, and it's equally simple. If f : X -> Y and S is a subset of X and T is a subset of Y, then the concept "f restricts to a function from S to T" can be said in the following two equivalent ways: f(S) subset T, or S subset f^{-1}(T). This is the `tendsto`

predicate on principal filters, it just says the image of set 1 is contained in set 2. image and preimage are adjoint functors between `set X`

and `set Y`

and because we're in this situation where all hom sets have size <= 1 (partially ordered sets like these complete lattices are categories with all hom sets having size <= 1) if you have two adjoint functors (or a Galois connection or however you want to think of it) then you get a predicate: either Hom(a,Phi b)=Hom(Psi a,b) has size 0 or size 1, and if it has size 1 then you say the predicate is satisfied. For filters this predicate is precisely `tendsto`

, and informally `tendsto f F G`

is the statement that the function f : X -> Y restricts to a function from the fuzzy set (F : filter X) to the fuzzy set (G : filter Y).

None of this point of view helps at all with your question! It's just that it helps me be a whole lot less scared by filters. In particular, when I was focussed on the underlying F.sets I would find the fact that <= was "backwards" really confusing -- thinking of filters as fuzzy subsets has completely eliminated this confusion.

#### Kevin Buzzard (Feb 22 2021 at 19:45):

A great example of a fuzzy set is the neighbourhood filter of a point in a topological space; the corresponding fuzzy set is an infinitesimal neighbourhood of the point in the sense of Isaac Newton. A function is continuous if the preimage of an infinitesimal nhd of f(a) contains an infinitesimal nhd of a and this is precisely `tendsto (N a) (N (f a))`

, or in other words f doesn't just map a to f(a), it maps the infinitesimal nhd of a to the infinitesimal nhd of f(a).

Sorry, I should go back to writing all this down in a blog post rather than here! In the mean time someone needs to come along and tell us how we're re-inventing the wheel with `filter.coprod`

.

#### Heather Macbeth (Feb 22 2021 at 20:33):

@Kevin Buzzard, mind if I add a proof of the `cocompact`

version and then open a PR? (Or feel free to do it yourself.)

#### Heather Macbeth (Feb 22 2021 at 20:35):

Obviously, we can close the PR if someone figures out how this is a wheel-reinvention :)

#### Bryan Gin-ge Chen (Feb 22 2021 at 20:37):

If you and Kevin have been reinventing the wheel all this time, then we surely need to better document the wheel!

#### Kevin Buzzard (Feb 22 2021 at 21:25):

Please feel free to open a PR! I have three open right now which is more than my usual max and so I'd rather not open another one. My proof is a typical Kevin meandering, probably it can be cleared up. @Patrick Massot is this already a thing?

#### Patrick Massot (Feb 22 2021 at 21:26):

I haven't followed. Is the question about golfing you last big code message?

#### Heather Macbeth (Feb 22 2021 at 21:28):

TL;DR Kevin defined a notion of coproduct of filters,

```
protected def coprod (f : filter α) (g : filter β) : filter (α × β) :=
f.comap prod.fst ⊔ g.comap prod.snd
```

which is useful for the original problem. Is this a known concept?

#### Kevin Buzzard (Feb 22 2021 at 21:29):

It differs from filter.prod because we use the join not the meet

#### Heather Macbeth (Feb 22 2021 at 21:29):

Its properties:

```
example : filter.coprod (cofinite : filter α) (cofinite : filter β) = cofinite := sorry
example : filter.coprod (cocompact α) (cocompact β) = cocompact (α × β) := sorry
example {α β γ δ} (a : filter α) (b : filter β) (c : filter γ) (d : filter δ) {f : α → γ} {g : β → δ}
(hf : tendsto f a c) (hg : tendsto g b d) :
tendsto (λ x : α × β, (f x.1, g x.2)) (a.coprod b) (c.coprod d) :=
sorry
```

#### Kevin Buzzard (Feb 22 2021 at 21:29):

The name might be wrong, we made it up

#### Patrick Massot (Feb 22 2021 at 21:30):

I've never seen this (and the same does feel wrong)

#### Patrick Massot (Feb 22 2021 at 21:31):

The name cocompact is also weird because it makes me think of groups acting with compact quotients. Is this new?

#### Heather Macbeth (Feb 22 2021 at 21:31):

#### Heather Macbeth (Feb 22 2021 at 21:32):

#### Patrick Massot (Feb 22 2021 at 21:33):

Oh, I merged that...

#### Patrick Massot (Feb 22 2021 at 21:33):

:older_man:

#### Heather Macbeth (Feb 22 2021 at 21:33):

Yury introduced it, but I found it useful today in order to work with proper maps (which are `tendsto _ cocompact cocompact`

)

#### Patrick Massot (Feb 22 2021 at 21:34):

I'm sure Kevin has another definition for proper maps...

#### Kevin Buzzard (Feb 22 2021 at 21:35):

But actually for complex varieties I think they coincide

#### Kevin Buzzard (Feb 22 2021 at 21:37):

For this coprod name, if S is a subset of X and T is a subset of Y then the coproduct is S x Y union X x T. Does this have a name in set land? Is it some kind of box construction or something?

#### Kevin Buzzard (Feb 22 2021 at 21:37):

(thinking of sets as principal filters)

#### Kevin Buzzard (Feb 22 2021 at 21:39):

It's complement of the product of the complements for sets, but unlike sets filters don't have this canonical complement antiautomorphism

#### Heather Macbeth (Feb 23 2021 at 00:15):

#6472, anyone should feel free to suggest a better name for the construction (or we can also just rewrite to refer to it as

```
f.comap prod.fst ⊔ g.comap prod.snd
```

throughout, without naming it).

#### Kevin Buzzard (Feb 23 2021 at 00:41):

Seems to me that `coprod`

has a natural meaning as a filter on alpha \coprod beta (push forward and then \lub). @Reid Barton do you know a good name for this construction?

#### Patrick Massot (Feb 23 2021 at 09:53):

The issue is that $\alpha \times \beta$ is *not* the coproduct in Type. The coproduct in Type is the sum type.

#### Patrick Massot (Feb 23 2021 at 09:54):

Also I think we can include in the PR

```
lemma principal_coprod_principal (s : set α) (t : set β) :
(𝓟 s).coprod (𝓟 t) = 𝓟 (sᶜ.prod tᶜ)ᶜ :=
begin
rw [filter.coprod, comap_principal, comap_principal, sup_principal],
congr,
ext x,
simp ; tauto,
end
```

#### Patrick Massot (Feb 23 2021 at 09:57):

And maybe it's a good time to start including counter-examples. Here we want an example with ` map (prod.map f g) (a.coprod b) < filter.prod (map f a) (map g b)`

. Using the above lemma you can make an example where all types are `fin 2`

.

#### Patrick Massot (Feb 23 2021 at 09:57):

Also the proof of the tendsto lemma can be reduced to `map_prod_map_coprod_le.trans (coprod_mono hf hg)`

#### Patrick Massot (Feb 23 2021 at 09:59):

And I still don't have a good name. Maybe `cross_prod`

since the case of principal filters is drawing a cross in the product space.

#### Kevin Buzzard (Feb 23 2021 at 13:29):

I had it in my head that there was a word for this in topology, like smash product or something, it's probably not that but in the set case this is surely construction which is useful to somebody

#### Heather Macbeth (Feb 23 2021 at 16:06):

Is this analogous? Given vector bundles $E_1$, $E_2$ over manifolds $M_1$, $M_2$ respectively, one has the projections $\pi_i:M_1\times M_2\to M_i$, and can pull back to vector bundles $\pi_i{}^*E_i$ over $M_1\times M_2$. One can then, in two ways, get a "combined" vector bundle over $M_1\times M_2$:

- $\pi_1{}^*E_1\otimes \pi_2{}^*E_2$ (which I have seen denoted $E_1\boxtimes E_2$)
- $\pi_1{}^*E_1\oplus \pi_2{}^*E_2$

Presumably there's a similar story for sheaves.

#### Adam Topaz (Feb 23 2021 at 16:36):

Maybe you should denote the second one with $\boxplus$?

#### Adam Topaz (Feb 23 2021 at 16:37):

I think this is the one which is analogous to the construction you were discussing, right?

#### Patrick Massot (Feb 26 2021 at 11:24):

@Heather Macbeth you requested my review but haven't integrated the above lemma and remove the equality question.

#### Kevin Buzzard (Feb 26 2021 at 11:41):

I really like how the proofs got even more golfed in the PR process :-)

#### Heather Macbeth (Feb 26 2021 at 15:17):

@Patrick Massot When you say "remove the equality question", this is by giving an example of

```
map (prod.map f g) (a.coprod b) < (map f a).coprod (map g b)
```

? In the discussion above you referred to an example with

```
map (prod.map f g) (a.coprod b) < (map f a).prod (map g b)
```

#### Patrick Massot (Feb 26 2021 at 20:01):

Oh sorry, this was a typo.

#### Patrick Massot (Feb 26 2021 at 20:01):

I meant `map (prod.map f g) (a.coprod b) < (map f a).coprod (map g b)`

#### Patrick Massot (Feb 26 2021 at 20:07):

I fear I lost the piece of paper where I wrote that counter-example. It was something like alpha = beta = gamma = delta = fin 2, f = id, g = lambda x, 1, a = b = principal {0].

#### Heather Macbeth (Feb 27 2021 at 03:43):

@Patrick Massot Thanks, indeed it works:

```
example {α β ι : Type*} (a : α) (b : β) (i : ι) :
(map (λ _ : α, b) (𝓟 {a})).coprod (map id (𝓟 {i}))
= 𝓟 (({b} : set β).prod (univ : set ι) ∪ (univ : set β).prod {i}) :=
begin
rw [map_principal, map_principal, principal_coprod_principal],
congr,
ext ⟨b', i'⟩,
simp,
tauto,
end
example {α β ι : Type*} (a : α) (b : β) (i : ι) :
map (prod.map (λ _ : α, b) id) ((𝓟 {a}).coprod (𝓟 {i}))
= 𝓟 (({b} : set β).prod (univ : set ι)) :=
begin
rw [principal_coprod_principal, map_principal],
congr,
ext ⟨b', i'⟩,
split,
{ rintros ⟨⟨a'', i''⟩, h₁, ⟨h₂, h₃⟩⟩,
simp },
{ rintros ⟨h₁, h₂⟩,
use (a, i'),
simpa using h₁.symm }
end
```

#### Heather Macbeth (Feb 27 2021 at 03:44):

Do we actually want this (a not-intrinsically-interesting counterexample) in mathlib? Maybe in archive or test?

#### Heather Macbeth (Feb 27 2021 at 03:50):

For now I just pushed the principal filter lemma and a description of the counterexample in words.

#### Patrick Massot (Feb 27 2021 at 08:30):

I would keep those as examples right after the inequality lemma. What would be really great would be to figure out how to use `slim_check`

for this kind of things. I'm sure most wrong results about filters have this kind of counter-examples.

#### Damiano Testa (Feb 27 2021 at 08:42):

Heather, I created a `counterexamples`

branch of mathlib, with a folder `counterexamples`

in `src`

: I am putting there the formalized counterexamples that I come across. There are two at the moment.

I'd be very happy if you wanted to contribute something there!

#### Heather Macbeth (Feb 27 2021 at 16:13):

@Damiano Testa For sure, I'll add it to the branch, is the plan to incorporate the branch into master at some point?

#### Damiano Testa (Feb 27 2021 at 16:15):

I think that it would be good if it appeared in mathlib, but I am happy to go with what everyone else also thinks is appropriate.

Personally, I find examples and counterexamples to be fundamental aspects of mathematics, so I would really like them to be in mathlib!

I remember many years ago reading books called `counterexamples in [topology/analysis/geometry]" and being fascinated by them!

#### Heather Macbeth (Feb 27 2021 at 16:42):

@Patrick Massot I pushed the counterexamples. @Damiano Testa I'll add them to the counterexamples branch once my PR is merged -- they rely on a new definition in the PR, `filter.coprod`

(or maybe it will be renamed).

#### Damiano Testa (Feb 27 2021 at 16:44):

Great! Of course there is no rush! I am very happy to see the counterexamples branch grow!

Last updated: May 17 2021 at 16:26 UTC