Funktionen

(Bei Quantoren ist hier ∊dom f nicht mitgeschrieben).  f: U→V bedeutet dom f = U und rng f⊆V.
Alles ist auch übertragbar auf funktionswertige Ausdrücke wie 3*x+1.           Mengendarstellung:
f ist Funktion ⇔ ∀x:∀u:∀v:(x,u)∊f∧(x,v)∊f → u=v y = f(x) ⇔ (x,y)∊f
x∊dom f ⇔ ∃y:(x,y)∊f y∊rng f ⇔ ∃x:(x,y)∊f

f=g ⇔ (dom f = dom g ∧∀x:f(x)=g(x))
y∊rng f ⇔ ∃x:f(x)=y
f injektiv: ⇔ (∀a:∀b: f(a)=f(b)→a=b  (bzw.⇔a=b))
f surjektiv B: ⇔ B=rng f ⇔ ∀b∊B;∃a:f(a)=b
y∊f(A)⇔∃x∊A:f(x)=y                  x∊f⁻¹(B)⇔f(x)∊B
x∊A⇒f(x)∊f(A);         wenn inj: x∊A⇔ f(x)∊f(A)
f(dom f) = rng f;   f⁻¹(rng f) = dom f
f(A)⊆rng f ;   f⁻¹(B)⊆dom f
A∩dom f=∅⇔f(A)=∅; B∩rng f=∅⇔f⁻¹(B)=∅;  		∀x∊dom f: φ(f(x)) ⇔ ∀y∊rng f: φ(y)
∀x∊A: φ(f(x)) ⇔ ∀y∊f(A): φ(y)
∀x∊f⁻¹(B): φ(f(x)) ⇔ ∀y∊B: φ(y)
∃x∊A: φ(f(x)) ⇔ ∃y∊f(A): φ(y)
∃x∊f⁻¹(B): φ(f(x)) ⇔ ∃y∊B: φ(y)
dabei B⊆rng f, A⊆dom f;
sonst ∊A∩dom f,∊B∩rng f
∀a∊A:∃b∊B:φ(a,b) ⇔
  ∃f:A→B:∀a∊A:φ(a,f(a))

dom f⁻¹ = rng f;  rng f⁻¹ = dom f  f⁻¹ bijektiv f⁻¹⁻¹=f
y∊f(A)⇔f⁻¹(y)∊A f⁻¹(f(x))=x f(f⁻¹(y))=y; y∊rng f

A⊆dom f bel sur inj  (sur:=B⊆rng f)
a = b ⇒ ⇔ f(a) = f(b)
x∊A ⇒ ⇔ f(x) ∊ f(A)
f⁻¹(f(A)) ⊇ = A; = w. satu f(f⁻¹(f(A))) = f(A)
f( f⁻¹(B)) ⊆ = B; = w. ∊ im f⁻¹(f( f⁻¹(B))) =f⁻¹(B)
A∩A'≠∅  ⇒ ⇔ f(A)∩f(A')≠∅
B∩B'≠∅ ⇐
 ⇔ f⁻¹(B)∩f⁻¹(B')≠∅ ( B∩B'∩rng)
A∩f⁻¹(B)≠∅ ⇔ f(A)∩B≠∅
A⊆A' ⇒ ⇔ f(A)⊆f(A')
B⊆B' ⇒ ⇔ f⁻¹(B)⊆f⁻¹(B')  (B∩rng⊆B')
f⁻¹(B)⊆A
⇒ ⇐,⇔ B⊆f(A)
f(A)⊆B ⇔ A⊆f⁻¹(B) f⁻¹(B)⊆A⇔B⊆Y-f(X-A)
f(A)⊆B ⇔ ∀x∊A:f(x)∊B
f(A∩A') ⊆ = f(A)∩f(A') f(⋂iAi) ⊆ ⋂if(Ai);   inj: =
f⁻¹(B∩B') = f⁻¹(B)∩f⁻¹(B') f⁻¹(⋂iAi) = ⋂if⁻¹(Ai)
f(A∪A') = f(A)∪f(A') f(⋃iAi) = ⋃if(Ai)
f⁻¹(B∪B') = f⁻¹(B)∪f⁻¹(B') f⁻¹(⋃iAi) = ⋃if⁻¹(Ai)
f(A-A') ⊇ = f(A)-f(A') f(AC)⊇f(A)C      Ω=dom/=rng
f⁻¹(B-B') = f⁻¹(B)-f⁻¹(B') f⁻¹(BC)=f⁻¹(B)C   Ω⊇rng/=dom
y∊f.(A)⇔f⁻¹ ({y})⊆A
⇔ ∀a:f(a)=y →y∊A
f.(A)=f(AC)C
f'':Pot(X)⇄Pot(Y):f⁻¹
f f'' f⁻¹
inj⇔ inj sur
sur⇔ sur inj
f (f○-) (-○f)
inj ⇔ ∀C: inj sur
sur ⇔ ∀C: sur inj
(f mon,retr,coret,epi)
f inj⇒(f(A)=f(A')⇒A=A')
f sur⇒(f⁻¹(B)=f⁻¹(B')⇒B=B')
(g○f)''=g''○f''; id''=id
(g○f)⁻¹=f⁻¹○g⁻¹; id⁻¹=id
f⁻¹(Y-B)=X-f⁻¹(B)
f⁻¹ ist boolalg hom.

g○f erlaubt, wenn dom(g)⊇rng f;   f inj ∧ g inj ⇒ g○f inj.;     f inj(A) ∧g inj (f(A))⇔g○f inj(A)
dom(g○f)=dom f;     rng(g○f) = g(rng f);      (h○g)○f = h○(g○f);    (g○f)(x) = g(f(x))
(g○f)⁻¹ = f⁻¹○g⁻¹;  (g○f)(A) = g(f(A));   (g○f)⁻¹(C)=f⁻¹(g⁻¹(C))
f inj(A):⇔  f∣A inj;      (∃f A→B:f inj) ⇔ (∃g B→A:g sur)          f○id|A=f;   id|B○f=f
g○f inj ⇒ f inj g○f sur ⇒ g sur f inj ⇒ (f○g=f○h ⇒ g=h) f sur ⇒ (g○f=h○f ⇒ g=h)
↑ + f sur ⇒ g  inj ↑ + g inj ⇒ f inj f inj ⇒ ∀g∃g':g'○f=g f sur ⇒∀g∃g':f○g'=g
f:A→B  inj⇔∃g:B→A:g○f = id|A;  sur⇔∃g:B→A:f○g = id|B;   bij⇔inj+sur⇔∃g:g○f=id&f○g = id