## Stream: general

### Topic: trouble defining filter base

#### Bernd Losert (Jan 11 2022 at 22:57):

I have the following code:

import tactic
import order.filter.partial
import order.filter.ultrafilter
import order.filter.bases
import algebra.support

noncomputable theory
open set function filter classical
open_locale classical filter

variables {X Y Z : Type*}

lemma ultrafilter_comap_set (f : X → Y) (A : set X) (𝒱 : ultrafilter Y) (h : f '' A ∈ 𝒱) :
∃ 𝒰 : ultrafilter X, 𝒰.map f = 𝒱 ∧ A ∈ 𝒰 := begin
let ℬ : filter_basis X := {
sets := { f ⁻¹' V ∩ A | V ∈ 𝒱 }, -- WHY DOES THIS NOT WORK?
nonempty := sorry,
inter_sets := sorry,
},
let ℱ := ℬ.filter,
haveI : ℱ.ne_bot := sorry,
let 𝒰 := ultrafilter.of ℱ,
use 𝒰,
have h : 𝒰.map f = 𝒱, sorry,
have h' : A ∈ 𝒰, sorry,
exact and.intro h h',
end


I can't figure out what the problem is though.

#### Reid Barton (Jan 11 2022 at 23:00):

Sadly, the syntax you are trying to use there simply does not exist.

#### Bernd Losert (Jan 11 2022 at 23:01):

Oh. What is the correct syntax then?

#### Reid Barton (Jan 11 2022 at 23:02):

You can write sets := { W | ∃ V ∈ 𝒱, W = f ⁻¹' V ∩ A },

#### Reid Barton (Jan 11 2022 at 23:02):

The thing before the | has to be a variable

#### Bernd Losert (Jan 11 2022 at 23:03):

Ah, I see. For some reason, I thought the set comprehension syntax was more flexible.

#### Yaël Dillies (Jan 11 2022 at 23:09):

Reid Barton said:

The thing before the | has to be a variable

or a ∈

#### Adam Topaz (Jan 11 2022 at 23:11):

That's not completely true... e.g.

import data.set.basic

variables {α β : Type*} (f : α → β) (S : set α)

def foo : set β := { (f x) | x ∈ S}

example : foo f S = { t | ∃ x ∈ S, f x = t } := rfl


#### Bernd Losert (Jan 11 2022 at 23:13):

Aha. So I tried { (f ⁻¹' V ∩ A) | V ∈ 𝒱 }, and that works.

Wait really??

#### Reid Barton (Jan 11 2022 at 23:15):

Aha, a "new" feature (added around 3.18 apparently)

#### Adam Topaz (Jan 11 2022 at 23:18):

Yep! This syntax was added fairly recently

#### Bernd Losert (Jan 11 2022 at 23:27):

It's weird that you have to add parentheses though.

#### Reid Barton (Jan 11 2022 at 23:36):

I assume it's because a variable is also an expression, but if we interpret it as an expression then the translation changes (it involves an existential and an equality).

Last updated: Aug 03 2023 at 10:10 UTC