search

metamath / set.mm

Metamath source file for logic and set theory
Other
254 stars 88 forks source link

Some typos/errors I found in Definition df-trkg 26259* #4147

Closed zwang123 closed 2 months ago

zwang123 commented 2 months ago

With this definition, the axiom A2 is actually equivalent to the transitivity of addition, eqtrd 2792.

addition -> equality

A1 A kind of reflexivity for the congruence relation (TarskiGC)

TarskiGC -> TarskiG_C

A8 Lower dimension axiom (DimTarskiG≥‘2) A9 Upper dimension axiom (V ∖ (DimTarskiG≥‘3))

DimTarskiG≥‘2 -> converse(DimTarskiG≥)‘‘{2} (V ∖ (DimTarskiG≥‘3)) -> (V ∖ (converse(DimTarskiG≥)‘‘{3}))

I think I can do a quick fix to this.