Properties

Properties - Predicates

definition
  let X, Y be set;
  pred X = Y means psi_1[X,Y];
  reflexivity
  proof
    thus for A being set holds psi_1[A,A];
  end;
end;

definition
  let X, Y be set;
  pred X = Y means
    phi_1[X,Y] if C1[X,Y],
    phi_2[X,Y] if C2[X,Y],
    phi_3[X,Y] if C3[X,Y]
    otherwise phi_4[X,Y];
  consistency;
  reflexivity
  proof
    let A be set;
    thus C1[A,A] implies phi_1[A,A];
    thus C2[A,A] implies phi_2[A,A];
    thus C3[A,A] implies phi_3[A,A];
    thus not C1[A,A] & not C2[A,A] & not C3[A,A] implies phi_4[A,A];
  end;
end;

definition
  let X, Y be set;
  pred X = Y means psi_1[X,Y];
  irreflexivity
  proof
    thus for A being set holds not psi_1[A,A];
  end;
end;

definition
  let X, Y be set;
  pred X = Y means
    phi_1[X,Y] if C1[X,Y],
    phi_2[X,Y] if C2[X,Y],
    phi_3[X,Y] if C3[X,Y]
    otherwise phi_4[X,Y];
  consistency;
  irreflexivity
  proof
    let A be set;
    thus not
    (
       (C1[A,A] implies phi_1[A,A]) &
       (C2[A,A] implies phi_2[A,A]) &
       (C3[A,A] implies phi_3[A,A]) &
       (not C1[A,A] & not C2[A,A] & not C3[A,A] implies phi_4[A,A])
    );
  end;
end;

definition
  let X, Y be set;
  pred X = Y means psi_1[X,Y];
  symmetry
  proof
    thus for A, B being set holds psi_1[A,B] implies psi_1[B,A];
  end;
end;

definition
  let X, Y be set;
  pred X = Y means
    phi_1[X,Y] if C1[X,Y],
    phi_2[X,Y] if C2[X,Y],
    phi_3[X,Y] if C3[X,Y]
    otherwise phi_4[X,Y];
  consistency;
  symmetry
  proof
    let A, B be set;
    thus 
      (C1[A,B] implies phi_1[A,B]) &
      (C2[A,B] implies phi_2[A,B]) &
      (C3[A,B] implies phi_3[A,B]) &
      (not C1[A,B] & not C2[A,B]& not C3[A,B] implies phi_4[A,B])
    implies 
      (C1[B,A] implies phi_1[B,A]) &
      (C2[B,A] implies phi_2[B,A]) &
      (C3[B,A] implies phi_3[B,A]) &
      (not C1[B,A] & not C2[B,A] & not C3[B,A] implies phi_4[B,A]);
  end;
end;

definition
  let X, Y be set;
  pred X = Y means psi_1[X,Y];
  asymmetry
  proof
    thus for A, B being set holds psi_1[A,B] implies not psi_1[B,A];
  end;
end;

definition
  let X, Y be set;
  pred X = Y means
    phi_1[X,Y] if C1[X,Y],
    phi_2[X,Y] if C2[X,Y],
    phi_3[X,Y] if C3[X,Y]
    otherwise phi_4[X,Y];
  consistency;
  asymmetry
  proof
    let A, B be set;
    thus 
      (C1[A,B] implies phi_1[A,B]) &
      (C2[A,B] implies phi_2[A,B]) &
      (C3[A,B] implies phi_3[A,B]) &
      (not C1[A,B] & not C2[A,B]& not C3[A,B] implies phi_4[A,B])
    implies
     not (
         (C1[B,A] implies phi_1[B,A]) &
         (C2[B,A] implies phi_2[B,A]) &
         (C3[B,A] implies phi_3[B,A]) &
         (not C1[B,A] & not C2[B,A] & not C3[B,A] implies phi_4[B,A])
     );
  end;
end;

definition
  let X, Y be set;
  pred X = Y means psi_1[X,Y];
  connectedness
  proof
    thus for A, B being set holds psi_1[A,B] or psi_1[B,A];
  end;
end;

definition
  let X, Y be set;
  pred X c= Y means
    phi_1[X,Y] if C1[X,Y],
    phi_2[X,Y] if C2[X,Y],
    phi_3[X,Y] if C3[X,Y]
    otherwise phi_4[X,Y];
  consistency;
  connectedness
  proof
    let A, B be set;
    thus 
      not (
          (C1[A,B] implies phi_1[A,B]) &
          (C2[A,B] implies phi_2[A,B]) &
          (C3[A,B] implies phi_3[A,B]) &
          (not C1[A,B] & not C2[A,B]& not C3[A,B] implies phi_4[A,B])
      )
    implies
         (C1[B,A] implies phi_1[B,A]) &
         (C2[B,A] implies phi_2[B,A]) &
         (C3[B,A] implies phi_3[B,A]) &
         (not C1[B,A] & not C2[B,A] & not C3[B,A] implies phi_4[B,A]);
  end;
end;

Properties - Functors

definition
  let X be set;
  func +X -> set means psi_1[it,X];
  existence;
  uniqueness;
  involutiveness
  proof
    thus for r, A being set st psi_1[r,A] holds psi_1[A,r];
  end;
end;

definition
  let X be set;
  func +X -> set means
    phi_1[it,X] if G1[X],
    phi_2[it,X] if G2[X],
    phi_3[it,X] if G3[X]
    otherwise phi_4[it,X];
  existence;
  uniqueness;
  consistency;
  involutiveness
  proof
    let IT, x be set;
    thus
      (G1[x] implies phi_1[IT,x]) &
      (G2[x] implies phi_2[IT,x]) &
      (G3[x] implies phi_3[IT,x]) &
      (not G1[x] & not G2[x] & not G3[x] implies phi_4[IT,x])
    implies
      (G1[IT] implies phi_1[x,IT]) &
      (G2[IT] implies phi_2[x,IT]) &
      (G3[IT] implies phi_3[x,IT]) &
      (not G1[IT] & not G2[IT] & not G3[IT] implies phi_4[x,IT]);
  end;
end;

definition
  let X be set;
  func +X -> set equals tau_1(X);
  coherence;
  involutiveness
  proof
    thus for r, A being set st r = tau_1(A) holds A = tau_1(r);
  end;
end;

definition
  let X be set;
  func +X -> set equals
    tau_1(X) if G1[X],
    tau_2(X) if G2[X],
    tau_3(X) if G3[X]
    otherwise tau_4(X);
  coherence;
  consistency;
  involutiveness
  proof
    let IT, x be set;
    thus 
      (G1[x] implies IT = tau_1(x)) &
      (G2[x] implies IT = tau_2(x)) &
      (G3[x] implies IT = tau_3(x)) &
      (not G1[x] & not G2[x] & not G3[x] implies IT = tau_4(x))
    implies
      (G1[IT] implies x = tau_1(IT)) &
      (G2[IT] implies x = tau_2(IT)) &
      (G3[IT] implies x = tau_3(IT)) &
      (not G1[IT] & not G2[IT] & not G3[IT] implies x = tau_4(IT));
  end;
end;

definition
  let X be set;
  func +X -> set means psi_1[it,X];
  existence;
  uniqueness;
  projectivity
  proof
    thus for r, A being set st psi_1[r,A] holds psi_1[r,r];
  end;
end;

definition
  let X be set;
  func +X -> set means
    phi_1[it,X] if G1[X],
    phi_2[it,X] if G2[X],
    phi_3[it,X] if G3[X]
    otherwise phi_4[it,X];
  existence;
  uniqueness;
  consistency;
  projectivity
  proof
    let IT, x be set;
    thus
      (G1[x] implies phi_1[IT,x]) &
      (G2[x] implies phi_2[IT,x]) &
      (G3[x] implies phi_3[IT,x]) &
      (not G1[x] & not G2[x] & not G3[x] implies phi_4[IT,x])
    implies
      (G1[IT] implies phi_1[IT,IT]) &
      (G2[IT] implies phi_2[IT,IT]) &
      (G3[IT] implies phi_3[IT,IT]) &
      (not G1[IT] & not G2[IT] & not G3[IT] implies phi_4[IT,IT]);
  end;
end;

definition
  let X be set;
  func +X -> set equals tau_1(X);
  coherence;
  projectivity
  proof
    thus for r, A being set st r = tau_1(A) holds r = tau_1(r);
  end;
end;

definition
  let X be set;
  func +X -> set equals
    tau_1(X) if G1[X],
    tau_2(X) if G2[X],
    tau_3(X) if G3[X]
    otherwise tau_4(X);
  coherence;
  consistency;
  projectivity
  proof
    let IT, x be set;
    thus 
      (G1[x] implies IT = tau_1(x)) &
      (G2[x] implies IT = tau_2(x)) &
      (G3[x] implies IT = tau_3(x)) &
      (not G1[x] & not G2[x] & not G3[x] implies IT = tau_4(x))
    implies
      (G1[IT] implies IT = tau_1(IT)) &
      (G2[IT] implies IT = tau_2(IT)) &
      (G3[IT] implies IT = tau_3(IT)) &
      (not G1[IT] & not G2[IT] & not G3[IT] implies IT = tau_4(IT));
  end;
end;

definition
  let X, Y be set;
  func X + Y -> set means psi_1[it,X,Y];
  existence;
  uniqueness;
  commutativity
  proof
    thus for r, A, B being set holds psi_1[r,A,B] implies psi_1[r,B,A];
  end;
end;

definition
  let X, Y be set;
  func X + Y -> set means
    psi_1[it,X,Y] if C1[X,Y],
    psi_2[it,X,Y] if C2[X,Y],
    psi_3[it,X,Y] if C3[X,Y]
    otherwise psi_4[it,X,Y];
  existence;
  uniqueness;
  consistency;
  commutativity
  proof
    let IT, x, y be set;
    thus
      (C1[x,y] implies psi_1[IT,x,y]) &
      (C2[x,y] implies psi_2[IT,x,y]) &
      (C3[x,y] implies psi_3[IT,x,y]) &
      (not C1[x,y] & not C2[x,y] & not C3[x,y] implies psi_4[IT,x,y])
    implies
      (C1[y,x] implies psi_1[IT,y,x]) &
      (C2[y,x] implies psi_2[IT,y,x]) &
      (C3[y,x] implies psi_3[IT,y,x]) &
      (not C1[y,x] & not C2[y,x] & not C3[y,x] implies psi_4[IT,y,x]);
  end;
end;

definition
  let X, Y be set;
  func X + Y -> set equals tau_1(X,Y);
  coherence;
  commutativity
  proof
    thus for r, A, B being set st r = tau_1(A,B) holds r = tau_1(B,A);
  end;
end;

definition
  let X, Y be set;
  func X + Y -> set equals
    tau_1(X,Y) if C1[X,Y],
    tau_2(X,Y) if C2[X,Y],
    tau_3(X,Y) if C3[X,Y]
    otherwise tau_4(X,Y);
  coherence;
  consistency;
  commutativity
  proof
    let IT, x, y be set;
    thus
      (C1[x,y] implies IT = tau_1(x,y)) &
      (C2[x,y] implies IT = tau_2(x,y)) &
      (C3[x,y] implies IT = tau_3(x,y)) &
      (not C1[x,y] & not C2[x,y] & not C3[x,y] implies IT = tau_4(x,y))
    implies
      (C1[y,x] implies IT = tau_1(y,x)) &
      (C2[y,x] implies IT = tau_2(y,x)) &
      (C3[y,x] implies IT = tau_3(y,x)) &
      (not C1[y,x] & not C2[y,x] & not C3[y,x] implies IT = tau_4(y,x));
  end;
end;

definition
  let X, Y be set;
  func X + Y -> set means psi_1[it,X,Y];
  existence;
  uniqueness;
  idempotence
  proof
    thus for A being set holds psi_1[A,A,A];
  end;
end;

definition
  let X, Y be set;
  func X + Y -> set means
    psi_1[it,X,Y] if C1[X,Y],
    psi_2[it,X,Y] if C2[X,Y],
    psi_3[it,X,Y] if C3[X,Y]
    otherwise psi_4[it,X,Y];
  existence;
  uniqueness;
  consistency;
  idempotence
  proof
    let IT be set;
    thus C1[IT,IT] implies psi_1[IT,IT,IT];
    thus C2[IT,IT] implies psi_2[IT,IT,IT];
    thus C3[IT,IT] implies psi_3[IT,IT,IT];
    thus not C1[IT,IT] & not C2[IT,IT] & not C3[IT,IT]
         implies psi_4[IT,IT,IT];
  end;
end;

definition
  let X, Y be set;
  func X + Y -> set equals F(X,Y);
  coherence;
  idempotence
  proof
    thus for A being set holds A = F(A,A);
  end;
end;

definition
  let X, Y be set;
  func X + Y -> set equals
    tau_1(X,Y) if C1[X,Y],
    tau_2(X,Y) if C2[X,Y],
    tau_3(X,Y) if C3[X,Y]
    otherwise tau_4(X,Y);
  coherence;
  consistency;
  idempotence
  proof
    let IT be set;
    thus C1[IT,IT] implies IT = tau_1(IT,IT);
    thus C2[IT,IT] implies IT = tau_2(IT,IT);
    thus C3[IT,IT] implies IT = tau_3(IT,IT);
    thus not C1[IT,IT] & not C2[IT,IT] & not C3[IT,IT]
         implies IT = tau_4(IT,IT);
  end;
end;