MapInvert

Inverting Maps.

Signature of MapInvert

List of Import References :
See BOOL
See DENOTATION
See Map
See Nat
See Option
See Pair
See Seq
See Set

SIGNATURE MapInvert[dom,   < : dom ** dom -> bool, 

$Date: 2010-09-30 18:24:17 +0200 (Do, 30. Sep 2010) $ ($Revision: 616 $)

                    codom, < : codom ** codom -> bool]

IMPORT Map[dom, <, codom] ONLY map
       Map[codom, <, dom] ONLY map

Parameter

dom is the type of the domain, dodom the type of the codomain. < is a total strict order: the formula ALL x y. ~(x < y) AND ~(y < x) => x === y must hold. As the old codomain is the new domain, we need also a strict order on the codomain.

SORT dom codom
FUN < : dom ** dom -> bool
FUN < : codom ** codom -> bool

Inverting Maps

Informally, invert{(d1->c1), (d2->c2), ... = {(c1->d1), (c2->d2), ...}}; invert is undefined, if m is not injective.

FUN invert: map[dom, <, codom] -> map[codom, <, dom]

next node: Maps,
prev node: MapCompose,
up to node: Subsystem Maps Proper