# Zulip Chat Archive

## Stream: new members

### Topic: Type theory construct

#### Dan Stanescu (Jul 08 2020 at 01:22):

Trying to formalize some notes by Pete Clark on filters I came up with a question mark. The problem is exemplified in the code below, which I tried to keep to a minimum. Basically the `principal_filter`

definition needs a proof that the set is not empty. If I try to use it later in `principal_of_finite`

, I want to obtain that there is such nonempty set, but then how do I feed that back into the same statement later on? In other words, how to fill the `_`

in the lemma statement?

```
import data.set.basic
import order.filter.basic
import tactic.basic
namespace peteClark
-- A filter is a non-empty collection of non-empty subsets of X with the following properties:
structure filter (X : Type) :=
( f_sets : set (set X) ) -- a collection of subsets of X
( f_nonempty : f_sets.nonempty )
( f_mem_nonempty : ∀ (A : set X), A ∈ f_sets → A.nonempty )
( f_mem_inter_in : ∀ (A B : set X), A ∈ f_sets ∧ B ∈ f_sets → A ∩ B ∈ f_sets )
( f_container_in : ∀ (A B : set X), A ∈ f_sets ∧ A ⊆ B → B ∈ f_sets )
( f_univ_in : set.univ ∈ f_sets )
variables {X : Type}
-- Example: a principal filter
def principal_filter (Y : set X) (hY : Y.nonempty) : filter X := sorry -- code not shown
variables (Xf : Type) [fintype Xf]
lemma principal_of_finite (F : filter Xf) :
∃ (Y : set Xf), Y.nonempty ∧ principal_filter Y _ = F := -- the underscore here??
begin -- should be the Y.nonempty from the first part
sorry, -- of the conjunction
end
end peteClark
```

This is probably not a desirable situation in type theory. I guess it's better not to ask for `Y.nonempty`

in `principal_filter`

, and that can easily be taken care of. I'm just wondering if there is a way to proceed in this setting. Any help appreciated!

#### Bryan Gin-ge Chen (Jul 08 2020 at 01:26):

Maybe you want:

```
lemma principal_of_finite (F : filter Xf) :
∃ (Y : set Xf), ∃ (hY : Y.nonempty), principal_filter Y hY = F
```

#### Dan Stanescu (Jul 08 2020 at 01:27):

I guess that is what I wanted! Thanks @Bryan Gin-ge Chen

#### Bhavik Mehta (Jul 08 2020 at 01:28):

Dan Stanescu said:

`( f_mem_inter_in : ∀ (A B : set X), A ∈ f_sets ∧ B ∈ f_sets → A ∩ B ∈ f_sets ) ( f_container_in : ∀ (A B : set X), A ∈ f_sets ∧ A ⊆ B → B ∈ f_sets )`

By the way, you can write these as `A ∈ f_sets → B ∈ f_sets → A ∩ B ∈ f_sets`

and `A ∈ f_sets → A ⊆ B → B ∈ f_sets`

which is sometimes easier to work with in practice!

#### Dan Stanescu (Jul 08 2020 at 01:29):

That one I knew, but I'm writing these to be legible by someone with zero knowledge of type theory.

#### Dan Stanescu (Jul 08 2020 at 01:29):

Or functional programming.

#### Dan Stanescu (Jul 08 2020 at 01:31):

Thank you both!

#### Patrick Massot (Jul 08 2020 at 08:46):

Having *both* `f_nonempty`

and `f_univ_in`

in the definition is a bit silly. Those conditions are equivalent using `f_container_in`

. And in pratice `f_univ_in`

is much more convenient both when constructing filters and when using the definition.

#### Patrick Massot (Jul 08 2020 at 08:48):

I'm almost sure you know but just to make sure: mathlib doesn't put `f_mem_non_empty`

in the definition of filters. So your definition is *not* equivalent to the definition in mathlib. Both choices have pros and cons, but mathlib's version is far superior in the long run (this is probably irrelevant to whatever you are trying to do).

#### Dan Stanescu (Jul 08 2020 at 09:08):

@Patrick Massot Thanks and agreed! I eventually default to `mathlib`

's version in my proofs. This was just me playing around preparing some formalization notes. Actually P. Clark doesn't have `f_univ_in`

in his definition, it just got there after I considered a few variants and I forgot to remove it. Then he only considers proper filters, there you go for `f_mem_non_empty`

.

#### Dan Stanescu (Jul 08 2020 at 09:13):

@Patrick Massot As a follow-up question, we don't seem to have nets in `mathlib`

. Would it make sense to add them?

#### Patrick Massot (Jul 08 2020 at 09:27):

If you plan to eventually use mathlib filters then you probably shouldn't put that properness condition in your main definition.

#### Patrick Massot (Jul 08 2020 at 09:29):

You are right that we don't have nets in mathlib. It seems that, beyond the illusion of familiarity that they provide at first, they are simply inferior to filters in every aspect. There is no harm in adding an isolated file `nets.lean`

, but I don't think we should start duplicating everything in those terms. Our topology library is already pretty big hence difficult to navigate.

#### Dan Stanescu (Jul 08 2020 at 11:34):

Patrick Massot said:

If you plan to eventually use mathlib filters then you probably shouldn't put that properness condition in your main definition.

Just making sure, proper filters in `mathlib`

are those `F`

such that `F ≠ ⊥`

--- ?

#### Yury G. Kudryashov (Jul 12 2020 at 04:34):

Yes, and many theorems assume `F ≠ ⊥`

.

#### Yury G. Kudryashov (Jul 12 2020 at 04:35):

As far as I understand, the main reason to deal with `⊥`

is to have a `complete_lattice`

structure.

#### Kevin Buzzard (Jul 12 2020 at 08:42):

It also enables you to do pushforwards and pullbacks (or `map`

and `comap`

as they're called in lean)

Last updated: May 08 2021 at 19:11 UTC