Nuprl Definition : fl-all
(∀i.phi) == fl-filter(phi;x.(¬binl i ∈b x) ∧b (¬binr i ∈b x))
Definitions occuring in Statement :
fl-filter: fl-filter(s;x.Q[x]),
deq-fset-member: a ∈b s,
union-deq: union-deq(A;B;a;b),
band: p ∧b q,
bnot: ¬bb,
inr: inr x ,
inl: inl x
Definitions occuring in definition :
fl-filter: fl-filter(s;x.Q[x]),
band: p ∧b q,
inl: inl x,
bnot: ¬bb,
deq-fset-member: a ∈b s,
union-deq: union-deq(A;B;a;b),
inr: inr x
FDL editor aliases :
fl-all
Latex:
(\mforall{}i.phi) == fl-filter(phi;x.(\mneg{}\msubb{}inl i \mmember{}\msubb{} x) \mwedge{}\msubb{} (\mneg{}\msubb{}inr i \mmember{}\msubb{} x))
Date html generated:
2020_05_20-AM-08_52_47
Last ObjectModification:
2016_01_15-PM-05_39_38
Theory : lattices
Home
Index