## Stream: general

### Topic: has_mem notation

#### Johan Commelin (Jan 14 2019 at 10:46):

Does anyone know how to fix this notation hack?

def covering_family {X : Type u} [category.{v} X] (U : X) : Type (max u v) :=
Π {{V}}, set (V ⟶ U)

local notation a ∈:50 b:50 := b a -- Aaahrg!

structure coverage (X : Type u) [category.{v} X] :=
(covers   : Π (U : X), set (covering_family U))
(property : ∀ {U V : X} (g : V ⟶ U),
∀ f ∈ covers U, ∃ h ∈ covers V,
∀ Vj (k : Vj ⟶ V), k ∈ h →
∃ Ui (l : Ui ⟶ U), l ∈ f ∧ ∃ m : Vj ⟶ Ui, m ≫ l = k ≫ g)


#### Johan Commelin (Jan 14 2019 at 10:46):

Ooh, and here is the relevant top of the file

import category_theory.presheaf
import category_theory.comma
import category_theory.full_subcategory
import analysis.topology.topological_space
import category_theory.examples.topological_spaces
import tactic.where

universes v u

namespace category_theory
open category_theory
open category_theory.limits


#### Chris Hughes (Jan 14 2019 at 10:49):

Could you do a has_mem instance instead?

#### Johan Commelin (Jan 14 2019 at 11:28):

No, I don't think has_mem works. I want to say that f : V ⟶ U is a member of c. But the type of f depends on V, which ranges over all of X.

Last updated: May 13 2021 at 22:15 UTC