Logiweb dictionary of EquivalenceRelations

Up Help

0 0 EquivalenceRelations 1 0 (⋯)

 2 0 Objekt-var
 3 0 Ex-var
 4 0 Ph-var
 5 0 Værdi
 6 0 Variabel

7 1 Op(∗) 8 2 Op(∗, ∗) 9 2 ∗ ¨= ∗ 10 1 ContainsEmpty(∗) 11 2 Dedu(∗, ∗) 12 2 Dedu_{0}(∗, ∗) 13 3 Dedu_{s}(∗, ∗, ∗) 14 3 Dedu_{1}(∗, ∗, ∗) 15 3 Dedu_{2}(∗, ∗, ∗) 16 4 Dedu_{3}(∗, ∗, ∗, ∗) 17 4 Dedu_{4}(∗, ∗, ∗, ∗) 18 4 Dedu_{4}^{∗}(∗, ∗, ∗, ∗) 19 3 Dedu_{5}(∗, ∗, ∗) 20 4 Dedu_{6}(∗, ∗, ∗, ∗) 21 4 Dedu_{6}^{∗}(∗, ∗, ∗, ∗) 22 1 Dedu_{7}(∗) 23 2 Dedu_{8}(∗, ∗) 24 2 Dedu_{8}^{∗}(∗, ∗) 25 0 Ex_{1} 26 0 Ex_{2} 27 0 Ex_{10} 28 0 Ex_{20} 29 1 ∗_{Ex} 30 1 ∗^{Ex} 31 4 ⟨∗≡ ∗ | ∗:=∗⟩_{Ex} 32 4 ⟨∗≡^{0} ∗ | ∗:=∗⟩_{Ex} 33 4 ⟨∗≡^{1} ∗ | ∗:=∗⟩_{Ex} 34 4 ⟨∗≡^{∗} ∗ | ∗:=∗⟩_{Ex} 35 0 ph_{1} 36 0 ph_{2} 37 0 ph_{3} 38 1 ∗_{Ph} 39 1 ∗^{Ph} 40 4 ⟨∗≡ ∗ | ∗:=∗⟩_{Ph} 41 4 ⟨∗≡^{0} ∗ | ∗:=∗⟩_{Ph} 42 4 ⟨∗≡^{1} ∗ | ∗:=∗⟩_{Ph} 43 4 ⟨∗≡^{∗} ∗ | ∗:=∗⟩_{Ph}

44 0 bs
45 0 OBS
46 0 BS

47 0 Ø 48 0 ZFsub 49 0 MP 50 0 Gen 51 0 Repetition 52 0 Neg 53 0 Ded 54 0 ExistIntro 55 0 Extensionality 56 0 Ødef 57 0 PairDef 58 0 UnionDef 59 0 PowerDef 60 0 SeparationDef 61 0 CheatAllDisjoint 62 0 AddDoubleNeg 63 0 RemoveDoubleNeg 64 0 AndCommutativity 65 0 AutoImply 66 0 Contrapositive 67 0 FirstConjunct 68 0 SecondConjunct 69 0 FromContradiction 70 0 FromDisjuncts 71 0 IffCommutativity 72 0 IffFirst 73 0 IffSecond 74 0 ImplyTransitivity 75 0 JoinConjuncts 76 0 MP2 77 0 MP3 78 0 MP4 79 0 MP5 80 0 MT 81 0 NegativeMT 82 0 Technicality 83 0 Weakening 84 0 WeakenOr1 85 0 WeakenOr2 86 0 Formula2Pair 87 0 Pair2Formula 88 0 Formula2Union 89 0 Union2Formula 90 0 Formula2Sep 91 0 Sep2Formula 92 0 SubsetInPower 93 0 HelperPowerIsSub 94 0 PowerIsSub 95 0 (Switch)HelperPowerIsSub 96 0 (Switch)PowerIsSub 97 0 ToSetEquality 98 0 HelperToSetEquality(t) 99 0 ToSetEquality(t) 100 0 HelperFromSetEquality 101 0 FromSetEquality 102 0 HelperReflexivity 103 0 Reflexivity 104 0 HelperSymmetry 105 0 Symmetry 106 0 HelperTransitivity 107 0 Transitivity 108 0 ERisReflexive 109 0 ERisSymmetric 110 0 ERisTransitive 111 0 ØisSubset 112 0 HelperMemberNotØ 113 0 MemberNotØ 114 0 HelperUniqueØ 115 0 UniqueØ 116 0 =Reflexivity 117 0 =Symmetry 118 0 Helper=Transitivity 119 0 =Transitivity 120 0 HelperTransferNotEq 121 0 TransferNotEq 122 0 HelperPairSubset 123 0 Helper(2)PairSubset 124 0 PairSubset 125 0 SamePair 126 0 SameSingleton 127 0 UnionSubset 128 0 SameUnion 129 0 SeparationSubset 130 0 SameSeparation 131 0 SameBinaryUnion 132 0 IntersectionSubset 133 0 SameIntersection 134 0 AutoMember 135 0 HelperEqSysNotØ 136 0 EqSysNotØ 137 0 HelperEqSubset 138 0 EqSubset 139 0 HelperEqNecessary 140 0 EqNecessary 141 0 HelperNoneEqNecessary 142 0 Helper(2)NoneEqNecessary 143 0 NoneEqNecessary 144 0 EqClassIsSubset 145 0 EqClassesAreDisjoint 146 0 AllDisjoint 147 0 AllDisjointImply 148 0 BSsubset 149 0 Union(BS/R)subset 150 0 UnionIdentity 151 0 EqSysIsPartition 152 2 ∗/∗ 153 2 ∗ ∩ ∗ 154 1 ∪∗ 155 2 ∗ ∪ ∗ 156 1 P(∗) 157 1 {∗} 158 2 {∗, ∗} 159 2 ⟨∗, ∗⟩ 160 2 ∗ ∈ ∗ 161 3 ∗(∗, ∗) 162 2 ReflRel(∗, ∗) 163 2 SymRel(∗, ∗) 164 2 TransRel(∗, ∗)

165 2 EqRel(∗, ∗) 166 3 [∗ ∈ ∗]_{∗} 167 2 Partition(∗, ∗) 168 2 ∗=∗ 169 2 ∗ ⊆ ∗ 170 1 ˙¬ ∗ 171 2 ∗ ∉ ∗ 172 2 ∗ ≠ ∗ 173 2 ∗ ˙∧ ∗ 174 2 ∗ ˙∨ ∗ 175 2 ∗ ˙⇔ ∗ 176 2 {ph ∈ ∗ | ∗}

The pyk compiler, version 0.grue.20060417+ by Klaus Grue GRD-2006-06-22.UTC:06:16:07.249053 = MJD-53908.TAI:06:16:40.249053 = LGT-4657673800249053e-6