Nuprl Definition : inv-rel
inv-rel(A;B;f;finv) ==
(∀a:A. ∀b:B. (((finv b) = (inl a) ∈ (A?)) ⇒ (b = (f a) ∈ B))) ∧ (∀a:A. ((finv (f a)) = (inl a) ∈ (A?)))
Definitions occuring in Statement :
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
unit: Unit,
apply: f a,
inl: inl x,
union: left + right,
equal: s = t ∈ T
Definitions occuring in definition :
and: P ∧ Q,
implies: P ⇒ Q,
all: ∀x:A. B[x],
equal: s = t ∈ T,
union: left + right,
unit: Unit,
apply: f a,
inl: inl x
FDL editor aliases :
inv-rel
Latex:
inv-rel(A;B;f;finv) ==
(\mforall{}a:A. \mforall{}b:B. (((finv b) = (inl a)) {}\mRightarrow{} (b = (f a)))) \mwedge{} (\mforall{}a:A. ((finv (f a)) = (inl a)))
Date html generated:
2016_05_15-PM-03_54_52
Last ObjectModification:
2015_09_23-AM-07_45_34
Theory : general
Home
Index