Nuprl Definition : vs-iso
A ≅ B == ∃f:A ⟶ B. ∃g:B ⟶ A. ((∀a:Point(A). ((g (f a)) = a ∈ Point(A))) ∧ (∀b:Point(B). ((f (g b)) = b ∈ Point(B))))
Definitions occuring in Statement :
vs-map: A ⟶ B,
vs-point: Point(vs),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
apply: f a,
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
vs-map: A ⟶ B,
and: P ∧ Q,
all: ∀x:A. B[x],
equal: s = t ∈ T,
vs-point: Point(vs),
apply: f a
FDL editor aliases :
vs-iso
Latex:
A \mcong{} B == \mexists{}f:A {}\mrightarrow{} B. \mexists{}g:B {}\mrightarrow{} A. ((\mforall{}a:Point(A). ((g (f a)) = a)) \mwedge{} (\mforall{}b:Point(B). ((f (g b)) = b)))
Date html generated:
2018_05_22-PM-09_43_15
Last ObjectModification:
2018_01_08-PM-09_08_38
Theory : linear!algebra
Home
Index