Notation idea

Stream: Is there code for X?

[Alex Kontorovich]

One point of friction from human mathematics to formalization is that we can't say things like: Let $U,V\subset\mathbb C$ and let $f:U\to V$, because $U,V$ aren't types. I wonder if there could be some notation to smooth this out? E.g.
The text "example (U V : Set \C) (f : U \longrightarrow V)" would "under the hood" produce

example (U V : Set ℂ) (f : ℂ → ℂ) (fUV: ∀ u ∈ U, f u ∈ V)

In other words, you would write:

example (U V : Set ℂ) (f : U ⟶ V)

but it would be interpreted as above. Might something like that make sense?... (Yes, it's a trivial point, but I'd think we'd want to remove as many friction points as possible, even the trivial ones?..)

[Felix Weilacher]

The second thing you write should already work. U and V will be interpreted as subtypes of C

[Mitchell Lee]

$U$ and $V$ are types. Or rather, they can already automatically be coerced to types; it's already possible to write f : U → V. But it's more idiomatic to write f : ℂ → ℂ (at least in the complex analysis part of mathlib), because it means you don't have to include the hypothesis fUV: ∀ u ∈ U, f u ∈ V unless it's necessary.

[Patrick Massot]

Note that fUV can already be spelled more compactly using docs#Set.MapsTo

[Patrick Massot]

And indeed using f : U → V and relying on the coercion from Set to Type is very painful.

[Mitchell Lee]

One way to do the thing you describe is by making U ⟶ V a structure, which carries the data of a function f : ℂ → ℂ and a proof that ∀ u ∈ U, f u ∈ V. This won't automatically expand the argument into two arguments like you want, but it would still be usable. However, I suspect that the burden of learning this new notation, and the difficulty in convincing everyone to use it rather than (f : ℂ → ℂ) (fUV: ∀ u ∈ U, f u ∈ V), would outweigh the minimal gains in the number of characters you have to type.

[Mitchell Lee]

(Also, this might be unnecessarily pedantic, but I think that U ⟶ V, defined as above, does not behave the way you might expect in all cases. Let A be any nonempty type and let B be any empty type. Let U : Set A and V : Set B be empty. Then, there is a function f : U → V, but there is no function f : A → B satisfying ∀ u ∈ U, f u ∈ V).

[Kyle Miller]

While we're here, there's a related notion of functions between filters (as filters are "generalized sets"). If you extract the definition morphisms from Pro(Set) and specialize it to filters, it looks like the following. You get both the idea of functions from one subset to another (Res below) as well as germs of functions at a point (Germ below).

import Mathlib

open scoped Filter Topology

structure Filter.Fun {α β : Type*} (F₁ : Filter α) (F₂ : Filter β) where
  toFun : α → β
  tendsto : Filter.Tendsto toFun F₁ F₂

infixr:25 " ⟶ " => Filter.Fun

variable {α β : Type*} (F₁ : Filter α) (F₂ : Filter β)

instance : CoeFun (F₁ ⟶ F₂) fun _ => α → β := ⟨Filter.Fun.toFun⟩

/-- Functions on filters are equivalent if they are eventually equal on the domain. -/
def Filter.Fun.eq {α β : Type*} (F₁ : Filter α) (F₂ : Filter β) (f g : F₁ ⟶ F₂) : Prop :=
  ∀ᶠ x in F₁, f x = g x

/-- Germs are functions on the neighborhood filter. `Filter.Fun.eq` is the expected equivalence relation for germs. -/
abbrev Germ {α : Type*} [TopologicalSpace α] (x : α) (β : Type*) := 𝓝 x ⟶ (⊤ : Filter β)

/-- Functions from `U` to `V`. -/
abbrev Res (U : Set α) (V : Set β) := 𝓟 U ⟶ 𝓟 V

[Adam Topaz]

What happens if \beta is empty (but alpha is not) and F_1 is \bot?

[Kyle Miller]

That's the pathological example that Mitchell mentioned in the comment right before mine.

[Adam Topaz]

Oh yeah I see it now.

[Adam Topaz]

(I for one don't think it's too pathological...)

[Eric Wieser]

Assuming your code doesn't handle that example, is there a version of Filter.Fun that does handle it in the case of general filters?

[Adam Topaz]

The only issue is that when alpha is nonempty and beta is empty then there are no functions from alpha to beta, but there should be a "function" from the empty filter on alpha to any filter on beta.

[Adam Topaz]

You could, for example, use a partial function from alpha to beta, and add some additional conditions to Filter.fun.

[Kyle Miller]

Yeah, I think partial functions are right (and also can be better since lots of times you don't want to bother with defining a function outside its domain). This might be the correct definition:

structure Filter.Fun {α β : Type*} (F₁ : Filter α) (F₂ : Filter β) where
  toFun : α → Option β
  tendsto : Filter.Tendsto toFun F₁ (F₂.map Option.some)

[Kyle Miller]

However, this goes in a direction that's not helpful for Alex's f : ℂ → ℂ.

[Kyle Miller]

But why worry about empty types. All types are inhabited, right? (That's how it is in Isabelle.)