Function - Mizar

In Mizar, if A and B are sets, we can form the type Function of A,B which describes something like \(f\colon A\to B\).

There is some subtlety here, because modern mathematics describes a function \(f\colon A\to B\) as a subset \(f\subset A\times B\) such that:

1. for each \(a\in A\), there exists a \(b\in B\) such that \((a,b)\in f\); and
2. for each \(a\in A\) and \(b_{1},b_{2}\in B\), if \((a,b_{1})\in f\) and \((a,b_{2})\in f\), then we have \(b_{1} = b_{2}\)

Mizar defines Function of X,Y as a quasi_total PartFunc of X,Y. A PartFunc of X,Y is defined as a Function-like Relation of X,Y, where Function-like literally encodes that second condition (uniqueness of image):

definition
  let X be set;
  attr X is Function-like means :Def1: :: FUNCT_1:def 1
  for x, y1, y2 being object
  st [x,y1] in X & [x,y2] in X
  holds y1 = y2;
end;

The Relation of X,Y is just a Subset of [:X,Y:] (a subset of \(X\times Y\)).

And quasi_total is defined as:

definition
  let X, Y be set;
  let R be Relation of X,Y;
  attr R is quasi_total means :Def1: :: FUNCT_2:def 1
  X = dom R if Y <> {}
  otherwise R = {};
  consistency;
end; 

This means that \(f\colon X\to\emptyset\) is implicitly empty, and therefore equal to \(\operatorname{id}_{\emptyset}\). Mizar proves this in Theorem FUNCT_2:130 (proving \(f\colon A\to\emptyset\implies f=\emptyset\)) and Theorem RELAT_1:55 (proving \(\operatorname{id}_{\emptyset}=\emptyset\)).

Sadly, a consequence of this choice, is that we often will need to include premises like "For any \(f\colon X\to Y\) such that (\(Y=\emptyset\implies X=\emptyset\)) we have \(P[f]\)".