[mizar] Bijection Gowers Example

[roland <roland_coghetto@hotmail.com>]

Paulson described on his website a translation in Isabelle/HOL of a
solution to an observation by Tim Gowers concerning bijection. 

I'll let you see more explanation on his link
(https://lawrencecpaulson.github.io/2024/02/28/Gowers_bijection_example
.html) as well as a proof in Lean by Alex Kontorovich.

Slawomir Kolodynski offers a proof in Isabelle/ZF deposited in the
IsarMathLib library (bij_def_alt)

I give you here a version in Mizar:

environ

 vocabularies RELAT_1, XBOOLE_0, FUNCT_1, TARSKI, SUBSET_1, FUNCT_2;
 notations TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2,
SUBSET_1;
 constructors RELSET_1, FUNCT_2;
 registrations XBOOLE_0, RELAT_1, FUNCT_1;
 requirements SUBSET, BOOLE;
 expansions TARSKI, FUNCT_1, FUNCT_2;
 theorems TARSKI, RELAT_1, FUNCT_1, XBOOLE_0, FUNCT_2;

begin

reserve X,Y for set;
reserve f for X-defined Y-valued Function;

theorem 
  f is bijective implies (for A being Subset of X holds f.:(X \ A) = Y
\ f.:A)
  proof
    assume
A1: f is bijective;
    let A be Subset of X;
A2: f.:(X \ A) = f.:X \ f.:A by A1,FUNCT_1:64;
    rng (f|X) = f.:X by RELAT_1:115;
    hence thesis by A1,A2,FUNCT_2:def 3;
  end;

theorem 
  (for A being Subset of X holds Y \ f.:A = f.:(X \ A)) implies
  f is bijective
  proof
    assume
A1: for A being Subset of X holds Y \ f.:A = f.:(X \ A);
    now
      {} c= X;
      hence {} is Subset of X;
      thus f.:{} = {};
      thus X \ {} = X;
    end;
    then
A2: Y \ {} = f.:X by A1;
    rng (f|X) = f.:X by RELAT_1:115;
    then
A3: f is onto by A2;
    f is one-to-one
    proof
      now
        let x,y be object;
        assume that
A4:     x in dom f and
A5:     y in dom f and
A6:     f.x = f.y;
        thus x = y
        proof
          assume
A7:       x <> y;
          x in X by A4;
          then {x} c= X by TARSKI:def 1;
          then
A8:       Y \ f.:{x} = f.: (X \ {x}) by A1;
          y in X & not y in {x} by A5,A7,TARSKI:def 1;
          then y in X \{x} by XBOOLE_0:def 5;
          then
A9:       f.y in Y \ f.:{x} by A8,A5,FUNCT_1:def 6;
          f.x <> f.y
          proof
            assume f.x = f.y;
            then
A10:        not f.x in f.:{x} by A9,XBOOLE_0:def 5;
            x in {x} by TARSKI:def 1;
            hence thesis by A10,A4,FUNCT_1:108;
          end;
          hence thesis by A6;
        end;
      end;
      hence thesis;
    end;
    hence thesis by A3;
end;

with a small, very elementary simplification:


theorem
  Y \ {} = f.:X &
  (for x being Element of X holds Y \ f.:{x} = f.: (X \ {x})) implies
  f is bijective
  proof
    assume that
A1: Y \ {} = f.:X and
A2: for x be Element of X holds Y \ f.:{x} = f.: (X \ {x});
    rng (f|X) = f.:X by RELAT_1:115;
    then
A3: f is onto by A1;
    f is one-to-one
    proof
      now
        let x,y be object;
        assume that
A4:     x in dom f and
A5:     y in dom f and
A6:     f.x = f.y;
        thus x = y
        proof
          assume
A7:       x <> y;
A8:       Y \ f.:{x} = f.: (X \ {x}) by A4,A2;
          y in X & not y in {x} by A5,A7,TARSKI:def 1;
          then y in X \ {x} by XBOOLE_0:def 5;
          then
A9:       f.y in Y \ f.:{x} by A8,A5,FUNCT_1:def 6;
          f.x <> f.y
          proof
            assume f.x = f.y;
            then
A10:        not f.x in f.:{x} by A9,XBOOLE_0:def 5;
            x in {x} by TARSKI:def 1;
            hence thesis by A10,A4,FUNCT_1:108;
          end;
          hence thesis by A6;
        end;
      end;
      hence thesis;
    end;
    hence thesis by A3;
end;

In the MML one of the propositions had already been proven in
JORDAN1K:15

Regards,
Roland