Nuprl Definition : transitive-set

We define ⌜transitive-set(s)⌝ using the ∀x∈s..... so that it will have
type ⌜ℙ⌝ rather than ⌜ℙ'⌝ (universe i+1)
if had been defined: ∀x:Set{i:l}. ((x ∈ s) ⇒ (x ⊆ s)).
But these are equivalent. See transitive-set-iff.⋅

transitive-set(s) == ∀x∈s.(x ⊆ s)

Definitions occuring in Statement : setsubset: (a ⊆ b), allsetmem: ∀a∈A.P[a]
Definitions occuring in definition : allsetmem: ∀a∈A.P[a], setsubset: (a ⊆ b)
FDL editor aliases : transitive-set

Latex:
transitive-set(s) == \mforall{}x\mmember{}s.(x \msubseteq{} s) Date html generated: 2018_07_29-AM-10_02_37 Last ObjectModification: 2018_05_30-AM-11_41_02 Theory : constructive!set!theory Home Index