Nuprl Definition : fdl-is-1
fdl-is-1(x) == (∃a∈x.isaxiom(a))_b
Definitions occuring in Statement :
bl-exists: (∃x∈L.P[x])_b,
bfalse: ff,
btrue: tt,
isaxiom: if z = Ax then a otherwise b
Definitions occuring in definition :
bl-exists: (∃x∈L.P[x])_b,
isaxiom: if z = Ax then a otherwise b,
btrue: tt,
bfalse: ff
FDL editor aliases :
fdl-is-1
Latex:
fdl-is-1(x) == (\mexists{}a\mmember{}x.isaxiom(a))\_b
Date html generated:
2020_05_20-AM-08_42_38
Last ObjectModification:
2017_01_24-PM-00_35_30
Theory : lattices
Home
Index