Logiweb codex of equivalence-relations in pyk
Up
Help
ref-1-id-22
var x
ref-0-id-0
equivalence-relations
ref-0-id-1
cdots
ref-0-id-2
object-var
ref-0-id-3
ex-var
ref-0-id-4
ph-var
ref-0-id-5
vaerdi
ref-0-id-6
variabel
ref-0-id-7
op {MissingArg} end op
ref-0-id-8
op2 {MissingArg} comma {MissingArg} end op2
ref-0-id-9
define-equal {MissingArg} comma {MissingArg} end equal
ref-0-id-10
contains-empty {MissingArg} end empty
ref-0-id-11
1deduction {MissingArg} conclude {MissingArg} end 1deduction
ref-0-id-12
1deduction zero {MissingArg} conclude {MissingArg} end 1deduction
ref-0-id-13
1deduction side {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
ref-0-id-14
1deduction one {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
ref-0-id-15
1deduction two {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
ref-0-id-16
1deduction three {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-17
1deduction four {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-18
1deduction four star {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-19
1deduction five {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-20
1deduction six {MissingArg} conclude {MissingArg} exception {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-21
1deduction six star {MissingArg} conclude {MissingArg} exception {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-22
1deduction seven {MissingArg} end 1deduction
ref-0-id-23
1deduction eight {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-24
1deduction eight star {MissingArg} bound {MissingArg} end 1deduction
ref-0-id-25
ex1
ref-0-id-26
ex2
ref-0-id-27
ex10
ref-0-id-28
ex20
ref-0-id-29
existential var {MissingArg} end var
ref-0-id-30
{MissingArg} is existential var
ref-0-id-31
exist-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-32
exist-sub0 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-33
exist-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-34
exist-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-35
placeholder-var1
ref-0-id-36
placeholder-var2
ref-0-id-37
placeholder-var3
ref-0-id-38
placeholder-var {MissingArg} end var
ref-0-id-39
{MissingArg} is placeholder-var
ref-0-id-40
ph-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-41
ph-sub0 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-42
ph-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-43
ph-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
ref-0-id-44
var big set
ref-0-id-45
object big set
ref-0-id-46
meta big set
ref-0-id-47
zermelo empty set
ref-0-id-48
system zf
ref-0-id-49
1rule mp
ref-0-id-50
1rule gen
ref-0-id-51
1rule repetition
ref-0-id-52
1rule ad absurdum
ref-0-id-53
1rule deduction
ref-0-id-54
1rule exist intro
ref-0-id-55
axiom extensionality
ref-0-id-56
axiom empty set
ref-0-id-57
axiom pair definition
ref-0-id-58
axiom union definition
ref-0-id-59
axiom power definition
ref-0-id-60
axiom separation definition
ref-0-id-61
cheating axiom all disjoint
ref-0-id-62
prop lemma add double neg
ref-0-id-63
prop lemma remove double neg
ref-0-id-64
prop lemma and commutativity
ref-0-id-65
prop lemma auto imply
ref-0-id-66
prop lemma contrapositive
ref-0-id-67
prop lemma first conjunct
ref-0-id-68
prop lemma second conjunct
ref-0-id-69
prop lemma from contradiction
ref-0-id-70
prop lemma from disjuncts
ref-0-id-71
prop lemma iff commutativity
ref-0-id-72
prop lemma iff first
ref-0-id-73
prop lemma iff second
ref-0-id-74
prop lemma imply transitivity
ref-0-id-75
prop lemma join conjuncts
ref-0-id-76
prop lemma mp2
ref-0-id-77
prop lemma mp3
ref-0-id-78
prop lemma mp4
ref-0-id-79
prop lemma mp5
ref-0-id-80
prop lemma mt
ref-0-id-81
prop lemma negative mt
ref-0-id-82
prop lemma technicality
ref-0-id-83
prop lemma weakening
ref-0-id-84
prop lemma weaken or first
ref-0-id-85
prop lemma weaken or second
ref-0-id-86
lemma formula2pair
ref-0-id-87
lemma pair2formula
ref-0-id-88
lemma formula2union
ref-0-id-89
lemma union2formula
ref-0-id-90
lemma formula2separation
ref-0-id-91
lemma separation2formula
ref-0-id-92
lemma subset in power set
ref-0-id-93
lemma power set is subset0
ref-0-id-94
lemma power set is subset
ref-0-id-95
lemma power set is subset0-switch
ref-0-id-96
lemma power set is subset-switch
ref-0-id-97
lemma set equality suff condition
ref-0-id-98
lemma set equality suff condition(t)0
ref-0-id-99
lemma set equality suff condition(t)
ref-0-id-100
lemma set equality skip quantifier
ref-0-id-101
lemma set equality nec condition
ref-0-id-102
lemma reflexivity0
ref-0-id-103
lemma reflexivity
ref-0-id-104
lemma symmetry0
ref-0-id-105
lemma symmetry
ref-0-id-106
lemma transitivity0
ref-0-id-107
lemma transitivity
ref-0-id-108
lemma er is reflexive
ref-0-id-109
lemma er is symmetric
ref-0-id-110
lemma er is transitive
ref-0-id-111
lemma empty set is subset
ref-0-id-112
lemma member not empty0
ref-0-id-113
lemma member not empty
ref-0-id-114
lemma unique empty set0
ref-0-id-115
lemma unique empty set
ref-0-id-116
lemma =reflexivity
ref-0-id-117
lemma =symmetry
ref-0-id-118
lemma =transitivity0
ref-0-id-119
lemma =transitivity
ref-0-id-120
lemma transfer ~is0
ref-0-id-121
lemma transfer ~is
ref-0-id-122
lemma pair subset0
ref-0-id-123
lemma pair subset1
ref-0-id-124
lemma pair subset
ref-0-id-125
lemma same pair
ref-0-id-126
lemma same singleton
ref-0-id-127
lemma union subset
ref-0-id-128
lemma same union
ref-0-id-129
lemma separation subset
ref-0-id-130
lemma same separation
ref-0-id-131
lemma same binary union
ref-0-id-132
lemma intersection subset
ref-0-id-133
lemma same intersection
ref-0-id-134
lemma auto member
ref-0-id-135
lemma eq-system not empty0
ref-0-id-136
lemma eq-system not empty
ref-0-id-137
lemma eq subset0
ref-0-id-138
lemma eq subset
ref-0-id-139
lemma equivalence nec condition0
ref-0-id-140
lemma equivalence nec condition
ref-0-id-141
lemma none-equivalence nec condition0
ref-0-id-142
lemma none-equivalence nec condition1
ref-0-id-143
lemma none-equivalence nec condition
ref-0-id-144
lemma equivalence class is subset
ref-0-id-145
lemma equivalence classes are disjoint
ref-0-id-146
lemma all disjoint
ref-0-id-147
lemma all disjoint-imply
ref-0-id-148
lemma bs subset union(bs/r)
ref-0-id-149
lemma union(bs/r) subset bs
ref-0-id-150
lemma union(bs/r) is bs
ref-0-id-151
theorem eq-system is partition
ref-0-id-152
eq-system of {MissingArg} modulo {MissingArg}
ref-0-id-153
intersection {MissingArg} comma {MissingArg} end intersection
ref-0-id-154
union {MissingArg} end union
ref-0-id-155
binary-union {MissingArg} comma {MissingArg} end union
ref-0-id-156
power {MissingArg} end power
ref-0-id-157
zermelo singleton {MissingArg} end singleton
ref-0-id-158
zermelo pair {MissingArg} comma {MissingArg} end pair
ref-0-id-159
zermelo ordered pair {MissingArg} comma {MissingArg} end pair
ref-0-id-160
{MissingArg} zermelo in {MissingArg}
ref-0-id-161
{MissingArg} is related to {MissingArg} under {MissingArg}
ref-0-id-162
{MissingArg} is reflexive relation in {MissingArg}
ref-0-id-163
{MissingArg} is symmetric relation in {MissingArg}
ref-0-id-164
{MissingArg} is transitive relation in {MissingArg}
ref-0-id-165
{MissingArg} is equivalence relation in {MissingArg}
ref-0-id-166
equivalence class of {MissingArg} in {MissingArg} modulo {MissingArg}
ref-0-id-167
{MissingArg} is partition of {MissingArg}
ref-0-id-168
{MissingArg} zermelo is {MissingArg}
ref-0-id-169
{MissingArg} is subset of {MissingArg}
ref-0-id-170
not0 {MissingArg}
ref-0-id-171
{MissingArg} zermelo ~in {MissingArg}
ref-0-id-172
{MissingArg} zermelo ~is {MissingArg}
ref-0-id-173
{MissingArg} and0 {MissingArg}
ref-0-id-174
{MissingArg} or0 {MissingArg}
ref-0-id-175
{MissingArg} iff {MissingArg}
ref-0-id-176
the set of ph in {MissingArg} such that {MissingArg} end set
The pyk compiler
, version 0.grue.20060417+ by
Klaus Grue
,
GRD-2006-08-24.UTC:08:13:50.904458
=
MJD-53971.TAI:08:14:23.904458
=
LGT-4663124063904458e-6