Nuprl Definition : distinct
distinct{s}(ps) == HTFor{<𝔹,∧b>} q::qs ∈ ps. ∀br(:|s|) ∈ qs. (¬b(r (=b) q))
Definitions occuring in Statement :
ball: ball,
mon_htfor: HTFor{g} h::t ∈ as. f[h; t],
bnot: ¬bb,
infix_ap: x f y,
band_mon: <𝔹,∧b>,
set_eq: =b,
set_car: |p|
Definitions occuring in definition :
mon_htfor: HTFor{g} h::t ∈ as. f[h; t],
band_mon: <𝔹,∧b>,
ball: ball,
set_car: |p|,
bnot: ¬bb,
infix_ap: x f y,
set_eq: =b
Latex:
distinct\{s\}(ps) == HTFor\{<\mBbbB{},\mwedge{}\msubb{}>\} q::qs \mmember{} ps. \mforall{}\msubb{}r(:|s|) \mmember{} qs. (\mneg{}\msubb{}(r (=\msubb{}) q))
Date html generated:
2016_05_16-AM-07_37_21
Last ObjectModification:
2015_09_23-AM-09_51_32
Theory : list_2
Home
Index