filter.comap

Stream: maths

[Yury G. Kudryashov]

Hi, I'm going to redefine docs#filter.comap this way:

def comap (f : α → β) (l : filter β) : filter α :=
{ sets             := {s | {y | ∀ ⦃x⦄, f x = y → x ∈ s} ∈ l},
  univ_sets        := univ_mem' $ λ y x hx, mem_univ x,
  sets_of_superset := λ s t Hs Hst, mem_of_superset Hs $ λ y hy x hx, Hst $ hy hx,
  inter_sets       := λ s t Hs Ht, mem_of_superset (inter_mem Hs Ht) $ λ y hy x hx,
    ⟨hy.1 hx, hy.2 hx⟩ }

Are there any objections?

[Patrick Massot]

What is the motivation?

[Yury G. Kudryashov]

My main motivation is to have s ∈ comap f l unfold to something ∈ l.

[Yury G. Kudryashov]

(though I can add lemmas instead)

[Patrick Massot]

Does it make a lot of proofs simpler? It's certainly harder to read when people jump to the definition.

[Yury G. Kudryashov]

I'll try. If it doesn't, then I'll revert to adding lemmas instead.

[Yury G. Kudryashov]

I definitely want to have

lemma compl_mem_comap : sᶜ ∈ comap f l ↔ (f '' s)ᶜ ∈ l :=

[Yury G. Kudryashov]

I'm going to add lemmas instead of changing the definition.