codiscrete within a set

Stream: mathlib4

[Daniel Weber]

Following this discussion in #14837, I'm creating this thread to discuss defining codiscreteWithin.
@Jireh Loreaux

[Jireh Loreaux]

Here are the relevant things I said on this PR (sorry for the week delay):

1. I think the definition of Filter.codiscrete should be migrated to mem_codiscrete', as it plays better with our API, and avoids a CoeSort in the definition.
2. I would prefer that we almost never talk about U ∈ codiscrete S where {S : Set X} {U : Set S}. Instead, I think we should create a new definition codiscreteWithin, much like nhdsWithin. I will describe this now.

The definition of t ∈ codiscrete X is (equivalent to) Disjoint (⨆ x : X, 𝓝[≠] x) (𝓟 tᶜ). I propose that we have, for s : Set X, codiscreteWithin s X where t ∈ codiscreteWithin s X means Disjoint (⨆ x ∈ s, 𝓝[≠] x) (𝓟 tᶜ). Note, I have not thought about whether there is a nice filter-level description of this (as with 𝓝[s] x := 𝓝 x ⊓ (𝓟 s)).

Note that if t : Set s, then t ∈ codiscrete s ↔ (Subtype.val '' tᶜ) ∈ codiscreteWithin s X.

[Jireh Loreaux]

Note that #14837 is awaiting the outcome of the discussion here, so your input is valuable.

[Jireh Loreaux]

Bumping to get more eyes on this. Maybe @Yury G. Kudryashov , Patrick Massot or @Floris van Doorn have an opinion.

[Floris van Doorn]

I agree that it's generally good to avoid subtypes, so codiscreteWithin seems good to have.