## 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.

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