Zulip Chat Archive

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.

Reid Barton (Jan 11 2022 at 23:14):

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