-
Notifications
You must be signed in to change notification settings - Fork 3
/
classes.dot
1380 lines (1380 loc) · 66.4 KB
/
classes.dot
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
digraph "instance_graph" {
size="30,30";
"ConditionallyCompleteLinearOrderedField" -> "InfSet";
"ConditionallyCompleteLinearOrderedField" -> "SupSet";
"ConditionallyCompleteLinearOrderedField" -> "Sup";
"ConditionallyCompleteLinearOrderedField" -> "ConditionallyCompleteLinearOrder";
"ConditionallyCompleteLinearOrderedField" -> "Inf";
"ConditionallyCompleteLinearOrderedField" -> "LinearOrderedField";
"ConditionallyCompleteLinearOrderedField" -> "Archimedean";
"BiheytingAlgebra" -> "CoheytingAlgebra";
"BiheytingAlgebra" -> "HNot";
"BiheytingAlgebra" -> "SDiff";
"BiheytingAlgebra" -> "HeytingAlgebra";
"UpgradedPolishSpace" -> "CompleteSpace";
"UpgradedPolishSpace" -> "MetricSpace";
"UpgradedPolishSpace" -> "TopologicalSpace.SecondCountableTopology";
"Nontrivial" -> "Nonempty";
"SeparatedSpace" -> "T3Space";
"Semigroup" -> "Dvd";
"Semigroup" -> "Mul";
"Semigroup" -> "IsJordan";
"CanonicallyLinearOrderedSemifield" -> "Nontrivial";
"CanonicallyLinearOrderedSemifield" -> "Inv";
"CanonicallyLinearOrderedSemifield" -> "Ord";
"CanonicallyLinearOrderedSemifield" -> "Max";
"CanonicallyLinearOrderedSemifield" -> "Div";
"CanonicallyLinearOrderedSemifield" -> "LinearOrderedCommGroupWithZero";
"CanonicallyLinearOrderedSemifield" -> "LinearOrderedSemifield";
"CanonicallyLinearOrderedSemifield" -> "Min";
"CanonicallyLinearOrderedSemifield" -> "CanonicallyLinearOrderedAddMonoid";
"CanonicallyLinearOrderedSemifield" -> "CanonicallyOrderedCommSemiring";
"StrictOrderedCommRing" -> "CommRing";
"StrictOrderedCommRing" -> "OrderedCommRing";
"StrictOrderedCommRing" -> "StrictOrderedRing";
"StrictOrderedCommRing" -> "StrictOrderedCommSemiring";
"TopologicalSpace.PseudoMetrizableSpace" -> "TopologicalSpace.FirstCountableTopology";
"OrderedCommGroup" -> "PartialOrder";
"OrderedCommGroup" -> "CommGroup";
"OrderedCommGroup" -> "OrderedCancelCommMonoid";
"Monoid" -> "Semigroup";
"Monoid" -> "One";
"Monoid" -> "MulOneClass";
"UniformSpace" -> "RegularSpace";
"UniformSpace" -> "TopologicalSpace";
"NonUnitalNonAssocRing" -> "Mul";
"NonUnitalNonAssocRing" -> "AddCommGroup";
"NonUnitalNonAssocRing" -> "HasDistribNeg";
"NonUnitalNonAssocRing" -> "NonUnitalNonAssocSemiring";
"LinearOrderedCancelAddCommMonoid" -> "Ord";
"LinearOrderedCancelAddCommMonoid" -> "Max";
"LinearOrderedCancelAddCommMonoid" -> "LinearOrderedAddCommMonoid";
"LinearOrderedCancelAddCommMonoid" -> "Min";
"LinearOrderedCancelAddCommMonoid" -> "OrderedCancelAddCommMonoid";
"SemigroupWithZero" -> "Semigroup";
"SemigroupWithZero" -> "MulZeroClass";
"SemigroupWithZero" -> "Zero";
"CategoryTheory.RegularMonoCategory" -> "CategoryTheory.StrongMonoCategory";
"Lattice" -> "SemilatticeInf";
"Lattice" -> "SemilatticeSup";
"Lattice" -> "Inf";
"BooleanAlgebra" -> "BiheytingAlgebra";
"BooleanAlgebra" -> "HImp";
"BooleanAlgebra" -> "HasCompl";
"BooleanAlgebra" -> "Bot";
"BooleanAlgebra" -> "DistribLattice";
"BooleanAlgebra" -> "ComplementedLattice";
"BooleanAlgebra" -> "GeneralizedBooleanAlgebra";
"BooleanAlgebra" -> "SDiff";
"BooleanAlgebra" -> "BoundedOrder";
"BooleanAlgebra" -> "Top";
"MeasurableInf₂" -> "MeasurableInf";
"OrderedCommMonoid" -> "PartialOrder";
"OrderedCommMonoid" -> "CommMonoid";
"NonarchimedeanAddGroup" -> "TopologicalAddGroup";
"CategoryTheory.Limits.HasZeroMorphisms" -> "CategoryTheory.Limits.MonoCoprod";
"IsDomain" -> "Nontrivial";
"IsDomain" -> "IsCancelMulZero";
"IsDomain" -> "CancelMonoidWithZero";
"NonUnitalSeminormedRing" -> "SeminormedAddCommGroup";
"NonUnitalSeminormedRing" -> "Norm";
"NonUnitalSeminormedRing" -> "ContinuousMul";
"NonUnitalSeminormedRing" -> "PseudoMetricSpace";
"NonUnitalSeminormedRing" -> "NonUnitalRing";
"NonUnitalSeminormedRing" -> "TopologicalRing";
"OrderedAddCommMonoid" -> "PartialOrder";
"OrderedAddCommMonoid" -> "AddCommMonoid";
"CompleteSemilatticeSup" -> "PartialOrder";
"CompleteSemilatticeSup" -> "SupSet";
"StandardBorelSpace" -> "MeasurableSingletonClass";
"StandardBorelSpace" -> "MeasurableSpace.CountablyGenerated";
"CommRing" -> "AddCommGroupWithOne";
"CommRing" -> "NonUnitalCommRing";
"CommRing" -> "CommSemiring";
"CommRing" -> "CommMonoid";
"CommRing" -> "Ring";
"LipschitzAdd" -> "ContinuousAdd";
"LinearOrderedAddCommGroupWithTop" -> "Nontrivial";
"LinearOrderedAddCommGroupWithTop" -> "SubNegMonoid";
"LinearOrderedAddCommGroupWithTop" -> "Neg";
"LinearOrderedAddCommGroupWithTop" -> "LinearOrderedAddCommMonoidWithTop";
"LinearOrderedAddCommGroupWithTop" -> "Sub";
"StrictOrderedSemiring" -> "Nontrivial";
"StrictOrderedSemiring" -> "NoMaxOrder";
"StrictOrderedSemiring" -> "PartialOrder";
"StrictOrderedSemiring" -> "OrderedSemiring";
"StrictOrderedSemiring" -> "CharZero";
"StrictOrderedSemiring" -> "OrderedCancelAddCommMonoid";
"StrictOrderedSemiring" -> "Semiring";
"TopologicalDivisionRing" -> "HasContinuousInv₀";
"TopologicalDivisionRing" -> "TopologicalRing";
"CategoryTheory.Noetherian" -> "CategoryTheory.EssentiallySmall";
"AddCommGroupWithOne" -> "One";
"AddCommGroupWithOne" -> "IntCast";
"AddCommGroupWithOne" -> "AddCommMonoidWithOne";
"AddCommGroupWithOne" -> "AddCommGroup";
"AddCommGroupWithOne" -> "NatCast";
"AddCommGroupWithOne" -> "AddGroupWithOne";
"One" -> "Nonempty";
"SeminormedAddCommGroup" -> "LipschitzAdd";
"SeminormedAddCommGroup" -> "SeminormedAddGroup";
"SeminormedAddCommGroup" -> "AddCommGroup";
"SeminormedAddCommGroup" -> "Norm";
"SeminormedAddCommGroup" -> "PseudoMetricSpace";
"SeminormedAddCommGroup" -> "TopologicalAddGroup";
"SeminormedAddCommGroup" -> "UniformAddGroup";
"TopologicalSpace.MetrizableSpace" -> "TopologicalSpace.PseudoMetrizableSpace";
"TopologicalSpace.MetrizableSpace" -> "T2Space";
"AddLeftCancelSemigroup" -> "AddSemigroup";
"AddLeftCancelSemigroup" -> "IsLeftCancelAdd";
"LinearOrderedCommGroup" -> "OrderedCommGroup";
"LinearOrderedCommGroup" -> "Ord";
"LinearOrderedCommGroup" -> "LinearOrder";
"LinearOrderedCommGroup" -> "Max";
"LinearOrderedCommGroup" -> "LinearOrderedCancelCommMonoid";
"LinearOrderedCommGroup" -> "Min";
"AddCancelCommMonoid" -> "AddLeftCancelMonoid";
"AddCancelCommMonoid" -> "AddCancelMonoid";
"AddCancelCommMonoid" -> "AddCommMonoid";
"CategoryTheory.RegularEpiCategory" -> "CategoryTheory.StrongEpiCategory";
"NormedCommRing" -> "SeminormedCommRing";
"NormedCommRing" -> "NormedRing";
"SeminormedCommRing" -> "CommRing";
"SeminormedCommRing" -> "SeminormedRing";
"TopologicalGroup" -> "RegularSpace";
"TopologicalGroup" -> "HSpace";
"TopologicalGroup" -> "ContinuousMul";
"TopologicalGroup" -> "ContinuousInv";
"TopologicalGroup" -> "ContinuousDiv";
"KleeneAlgebra" -> "KStar";
"KleeneAlgebra" -> "IdemSemiring";
"Quandle" -> "Rack";
"TopologicalSpace.FirstCountableTopology" -> "FrechetUrysohnSpace";
"OrderedRing" -> "PartialOrder";
"OrderedRing" -> "OrderedSemiring";
"OrderedRing" -> "OrderedAddCommGroup";
"OrderedRing" -> "Ring";
"CategoryTheory.IsCofiltered" -> "CategoryTheory.IsCofilteredOrEmpty";
"IsLowerModularLattice" -> "IsWeakLowerModularLattice";
"CategoryTheory.FinitaryExtensive" -> "CategoryTheory.Limits.HasFiniteCoproducts";
"CategoryTheory.FinitaryExtensive" -> "CategoryTheory.Limits.HasStrictInitialObjects";
"LinearOrderedCommSemiring" -> "LinearOrderedCancelAddCommMonoid";
"LinearOrderedCommSemiring" -> "Ord";
"LinearOrderedCommSemiring" -> "Max";
"LinearOrderedCommSemiring" -> "Min";
"LinearOrderedCommSemiring" -> "StrictOrderedCommSemiring";
"LinearOrderedCommSemiring" -> "LinearOrderedSemiring";
"DiscreteTopology" -> "TopologicalSpace.MetrizableSpace";
"DiscreteTopology" -> "TopologicalSpace.FirstCountableTopology";
"DiscreteTopology" -> "AlexandrovDiscrete";
"DiscreteTopology" -> "T2Space";
"DiscreteTopology" -> "TotallySeparatedSpace";
"DiscreteTopology" -> "LocallyConnectedSpace";
"NormedGroup" -> "SeminormedGroup";
"NormedGroup" -> "Group";
"NormedGroup" -> "Norm";
"NormedGroup" -> "MetricSpace";
"CategoryTheory.Extensive" -> "CategoryTheory.Limits.HasFiniteCoproducts";
"CategoryTheory.Extensive" -> "CategoryTheory.HasPullbacksOfInclusions";
"LinearOrder" -> "Lattice";
"LinearOrder" -> "Ord";
"LinearOrder" -> "Max";
"LinearOrder" -> "PartialOrder";
"LinearOrder" -> "Min";
"LinearOrder" -> "DistribLattice";
"Topology.IsUpperSet" -> "AlexandrovDiscrete";
"SeminormedGroup" -> "Group";
"SeminormedGroup" -> "NNNorm";
"SeminormedGroup" -> "Norm";
"SeminormedGroup" -> "PseudoMetricSpace";
"CategoryTheory.Limits.HasFiniteLimits" -> "CategoryTheory.Limits.HasFiniteProducts";
"Finite" -> "Countable";
"Unique" -> "Fintype";
"Unique" -> "Inhabited";
"Unique" -> "Subsingleton";
"ConditionallyCompleteLinearOrderBot" -> "OrderBot";
"ConditionallyCompleteLinearOrderBot" -> "Bot";
"ConditionallyCompleteLinearOrderBot" -> "ConditionallyCompleteLinearOrder";
"CategoryTheory.Limits.HasFiniteBiproducts" -> "CategoryTheory.Limits.HasFiniteCoproducts";
"CategoryTheory.Limits.HasFiniteBiproducts" -> "CategoryTheory.Limits.HasZeroObject";
"CategoryTheory.Limits.HasFiniteBiproducts" -> "CategoryTheory.Limits.HasFiniteProducts";
"InvolutiveStar" -> "Star";
"StarMul" -> "InvolutiveStar";
"NormalizedGCDMonoid" -> "GCDMonoid";
"NormalizedGCDMonoid" -> "NormalizationMonoid";
"Topology.IsLowerSet" -> "AlexandrovDiscrete";
"CancelCommMonoidWithZero" -> "IsLeftCancelMulZero";
"CancelCommMonoidWithZero" -> "CommMonoidWithZero";
"CancelCommMonoidWithZero" -> "CancelMonoidWithZero";
"SeminormedAddGroup" -> "NNNorm";
"SeminormedAddGroup" -> "Norm";
"SeminormedAddGroup" -> "PseudoMetricSpace";
"SeminormedAddGroup" -> "AddGroup";
"NonemptyFiniteLinearOrder" -> "LinearOrder";
"NonemptyFiniteLinearOrder" -> "Fintype";
"NonemptyFiniteLinearOrder" -> "Nonempty";
"NonemptyFiniteLinearOrder" -> "BoundedOrder";
"DivisionCommMonoid" -> "DivisionMonoid";
"DivisionCommMonoid" -> "CommMonoid";
"GroupWithZero" -> "Nontrivial";
"GroupWithZero" -> "Inv";
"GroupWithZero" -> "DivisionMonoid";
"GroupWithZero" -> "Div";
"GroupWithZero" -> "DivInvMonoid";
"GroupWithZero" -> "MonoidWithZero";
"GroupWithZero" -> "NoZeroDivisors";
"GroupWithZero" -> "CancelMonoidWithZero";
"Rack" -> "Shelf";
"CompleteAtomicBooleanAlgebra" -> "HImp";
"CompleteAtomicBooleanAlgebra" -> "CompletelyDistribLattice";
"CompleteAtomicBooleanAlgebra" -> "CompleteBooleanAlgebra";
"CompleteAtomicBooleanAlgebra" -> "HasCompl";
"CompleteAtomicBooleanAlgebra" -> "IsCoatomistic";
"CompleteAtomicBooleanAlgebra" -> "SDiff";
"CompleteAtomicBooleanAlgebra" -> "IsAtomistic";
"IsSimpleOrder" -> "Nontrivial";
"NormedLatticeAddCommGroup" -> "Lattice";
"NormedLatticeAddCommGroup" -> "TopologicalLattice";
"NormedLatticeAddCommGroup" -> "ContinuousSup";
"NormedLatticeAddCommGroup" -> "OrderClosedTopology";
"NormedLatticeAddCommGroup" -> "ContinuousInf";
"NormedLatticeAddCommGroup" -> "HasSolidNorm";
"NormedLatticeAddCommGroup" -> "OrderedAddCommGroup";
"NormedLatticeAddCommGroup" -> "NormedAddCommGroup";
"ConditionallyCompleteLattice" -> "Lattice";
"ConditionallyCompleteLattice" -> "InfSet";
"ConditionallyCompleteLattice" -> "SupSet";
"IsCancelMul" -> "IsLeftCancelMul";
"IsCancelMul" -> "IsRightCancelMul";
"CategoryTheory.Limits.HasColimitsOfSize" -> "CategoryTheory.Limits.HasFiniteColimits";
"GeneralizedCoheytingAlgebra" -> "Lattice";
"GeneralizedCoheytingAlgebra" -> "OrderBot";
"GeneralizedCoheytingAlgebra" -> "Bot";
"GeneralizedCoheytingAlgebra" -> "DistribLattice";
"GeneralizedCoheytingAlgebra" -> "SDiff";
"CategoryTheory.NonPreadditiveAbelian" -> "CategoryTheory.Limits.HasZeroMorphisms";
"CategoryTheory.NonPreadditiveAbelian" -> "CategoryTheory.Limits.HasFiniteCoproducts";
"CategoryTheory.NonPreadditiveAbelian" -> "CategoryTheory.Limits.HasCokernels";
"CategoryTheory.NonPreadditiveAbelian" -> "CategoryTheory.NormalMonoCategory";
"CategoryTheory.NonPreadditiveAbelian" -> "CategoryTheory.Limits.HasZeroObject";
"CategoryTheory.NonPreadditiveAbelian" -> "CategoryTheory.Limits.HasKernels";
"CategoryTheory.NonPreadditiveAbelian" -> "CategoryTheory.NormalEpiCategory";
"CategoryTheory.NonPreadditiveAbelian" -> "CategoryTheory.Limits.HasFiniteProducts";
"WithIdeal" -> "UniformSpace";
"WithIdeal" -> "TopologicalSpace";
"WithIdeal" -> "NonarchimedeanRing";
"WithIdeal" -> "UniformAddGroup";
"Group" -> "DivisionMonoid";
"Group" -> "DivInvMonoid";
"Group" -> "CancelMonoid";
"CompleteDistribLattice" -> "Order.Coframe";
"CompleteDistribLattice" -> "Order.Frame";
"MeasurableSub₂" -> "MeasurableSub";
"SubNegMonoid" -> "Neg";
"SubNegMonoid" -> "AddMonoid";
"SubNegMonoid" -> "Sub";
"DivInvOneMonoid" -> "DivInvMonoid";
"DivInvOneMonoid" -> "InvOneClass";
"GroupFilterBasis" -> "TopologicalGroup";
"UpgradedStandardBorel" -> "BorelSpace";
"UpgradedStandardBorel" -> "MeasurableSpace";
"UpgradedStandardBorel" -> "TopologicalSpace";
"UpgradedStandardBorel" -> "PolishSpace";
"IsCommJordan" -> "IsJordan";
"CategoryTheory.Abelian" -> "CategoryTheory.IsIdempotentComplete";
"CategoryTheory.Abelian" -> "CategoryTheory.Limits.HasFiniteLimits";
"CategoryTheory.Abelian" -> "CategoryTheory.Limits.HasStrongEpiMonoFactorisations";
"CategoryTheory.Abelian" -> "CategoryTheory.Limits.HasCokernels";
"CategoryTheory.Abelian" -> "CategoryTheory.Preadditive";
"CategoryTheory.Abelian" -> "CategoryTheory.NormalMonoCategory";
"CategoryTheory.Abelian" -> "CategoryTheory.Limits.HasZeroObject";
"CategoryTheory.Abelian" -> "CategoryTheory.Limits.HasKernels";
"CategoryTheory.Abelian" -> "CategoryTheory.CategoryWithHomology";
"CategoryTheory.Abelian" -> "CategoryTheory.Limits.HasBinaryBiproducts";
"CategoryTheory.Abelian" -> "CategoryTheory.NormalEpiCategory";
"CategoryTheory.Abelian" -> "CategoryTheory.Limits.HasFiniteProducts";
"CategoryTheory.Abelian" -> "CategoryTheory.Limits.HasFiniteColimits";
"OrderBot" -> "Bot";
"AddLeftCancelMonoid" -> "AddLeftCancelSemigroup";
"AddLeftCancelMonoid" -> "AddMonoid";
"AddLeftCancelMonoid" -> "Zero";
"LipschitzMul" -> "ContinuousMul";
"AddCommMonoidWithOne" -> "AddCommMonoid";
"AddCommMonoidWithOne" -> "AddMonoidWithOne";
"MulZeroClass" -> "Mul";
"MulZeroClass" -> "Zero";
"RingFilterBasis" -> "AddGroupFilterBasis";
"RingFilterBasis" -> "TopologicalRing";
"IsUpperModularLattice" -> "IsWeakUpperModularLattice";
"LinearOrderedRing" -> "IsDomain";
"LinearOrderedRing" -> "Ord";
"LinearOrderedRing" -> "LinearOrder";
"LinearOrderedRing" -> "Max";
"LinearOrderedRing" -> "Min";
"LinearOrderedRing" -> "NoZeroDivisors";
"LinearOrderedRing" -> "LinearOrderedAddCommGroup";
"LinearOrderedRing" -> "StrictOrderedRing";
"LinearOrderedRing" -> "LinearOrderedSemiring";
"BorelSpace" -> "OpensMeasurableSpace";
"AddCancelMonoid" -> "AddLeftCancelMonoid";
"AddCancelMonoid" -> "AddRightCancelMonoid";
"AddCancelMonoid" -> "IsCancelAdd";
"UniformGroup" -> "TopologicalGroup";
"PartialOrder" -> "Preorder";
"CategoryTheory.Groupoid" -> "Quiver.HasInvolutiveReverse";
"CategoryTheory.Groupoid" -> "CategoryTheory.Category";
"AddCommGroup" -> "AddCancelCommMonoid";
"AddCommGroup" -> "AddCommMonoid";
"AddCommGroup" -> "AddGroup";
"AddCommGroup" -> "SubtractionCommMonoid";
"DivisionMonoid" -> "DivInvOneMonoid";
"DivisionMonoid" -> "InvolutiveInv";
"DivisionMonoid" -> "DivInvMonoid";
"RankCondition" -> "InvariantBasisNumber";
"NormedLinearOrderedField" -> "Norm";
"NormedLinearOrderedField" -> "NormedField";
"NormedLinearOrderedField" -> "MetricSpace";
"NormedLinearOrderedField" -> "LinearOrderedField";
"InfSet" -> "Nonempty";
"OrderedSemiring" -> "OrderedAddCommMonoid";
"OrderedSemiring" -> "PartialOrder";
"OrderedSemiring" -> "ZeroLEOneClass";
"OrderedSemiring" -> "Semiring";
"CoheytingAlgebra" -> "GeneralizedCoheytingAlgebra";
"CoheytingAlgebra" -> "DistribLattice";
"CoheytingAlgebra" -> "HNot";
"CoheytingAlgebra" -> "BoundedOrder";
"CoheytingAlgebra" -> "Top";
"Semifield" -> "Nontrivial";
"Semifield" -> "Inv";
"Semifield" -> "Div";
"Semifield" -> "CommSemiring";
"Semifield" -> "DivisionSemiring";
"Semifield" -> "CommGroupWithZero";
"CategoryTheory.Bicategory.Strict" -> "CategoryTheory.Category";
"ContractibleSpace" -> "SimplyConnectedSpace";
"ContractibleSpace" -> "PathConnectedSpace";
"CanonicallyOrderedMonoid" -> "OrderedCommMonoid";
"CanonicallyOrderedMonoid" -> "ExistsMulOfLE";
"CanonicallyOrderedMonoid" -> "OrderBot";
"CanonicallyOrderedMonoid" -> "Bot";
"CompletelyDistribLattice" -> "CompleteDistribLattice";
"CompletelyDistribLattice" -> "CompleteLattice";
"CircularPreorder" -> "Btw";
"CircularPreorder" -> "SBtw";
"CategoryTheory.SplitMonoCategory" -> "CategoryTheory.RegularMonoCategory";
"CompleteBooleanAlgebra" -> "BooleanAlgebra";
"CompleteBooleanAlgebra" -> "CompleteDistribLattice";
"CompleteBooleanAlgebra" -> "InfSet";
"CompleteBooleanAlgebra" -> "SupSet";
"LocalRing" -> "Nontrivial";
"IsSimpleGroup" -> "Nontrivial";
"Setoid" -> "HasEquiv";
"UniqueFactorizationMonoid" -> "WfDvdMonoid";
"CategoryTheory.Limits.HasStrongEpiMonoFactorisations" -> "CategoryTheory.Limits.HasImages";
"CategoryTheory.Limits.HasStrongEpiMonoFactorisations" -> "CategoryTheory.Limits.HasStrongEpiImages";
"TopologicalLattice" -> "ContinuousSup";
"TopologicalLattice" -> "ContinuousInf";
"NonUnitalNormedRing" -> "NonUnitalSeminormedRing";
"NonUnitalNormedRing" -> "Norm";
"NonUnitalNormedRing" -> "MetricSpace";
"NonUnitalNormedRing" -> "NonUnitalRing";
"NonUnitalNormedRing" -> "NormedAddCommGroup";
"NonAssocRing" -> "NonUnitalNonAssocRing";
"NonAssocRing" -> "AddCommGroupWithOne";
"NonAssocRing" -> "One";
"NonAssocRing" -> "IntCast";
"NonAssocRing" -> "NatCast";
"NonAssocRing" -> "NonAssocSemiring";
"LawfulFix" -> "Fix";
"Topology.IsLower" -> "ClosedIciTopology";
"NonUnitalCommRing" -> "CommSemigroup";
"NonUnitalCommRing" -> "NonUnitalRing";
"NonUnitalCommRing" -> "NonUnitalCommSemiring";
"SupSet" -> "Nonempty";
"LinearOrderedAddCommMonoid" -> "OrderedAddCommMonoid";
"LinearOrderedAddCommMonoid" -> "LinearOrder";
"LinearOrderedAddCommMonoid" -> "AddCommMonoid";
"Bot" -> "Nonempty";
"CategoryTheory.Artinian" -> "CategoryTheory.EssentiallySmall";
"CompletableTopField" -> "SeparatedSpace";
"MulZeroOneClass" -> "MulZeroClass";
"MulZeroOneClass" -> "MulOneClass";
"MulZeroOneClass" -> "Zero";
"Topology.IsUpper" -> "ClosedIicTopology";
"CommGroup" -> "IsSolvable";
"CommGroup" -> "DivisionCommMonoid";
"CommGroup" -> "Group";
"CommGroup" -> "Group.IsNilpotent";
"CommGroup" -> "CommMonoid";
"CommGroup" -> "CancelCommMonoid";
"DiscreteValuationRing" -> "LocalRing";
"DiscreteValuationRing" -> "IsPrincipalIdealRing";
"DiscreteValuationRing" -> "ValuationRing";
"ProperSpace" -> "CompleteSpace";
"ProperSpace" -> "TopologicalSpace.SecondCountableTopology";
"ProperSpace" -> "LocallyCompactSpace";
"CategoryTheory.Limits.HasLimitsOfSize" -> "CategoryTheory.Limits.HasFiniteLimits";
"IsEmpty" -> "Fintype";
"IsEmpty" -> "Subsingleton";
"IsEmpty" -> "Encodable";
"Std.ToFormat" -> "Lean.ToMessageData";
"IsCancelMulZero" -> "IsLeftCancelMulZero";
"IsCancelMulZero" -> "IsRightCancelMulZero";
"LinearOrderedCommGroupWithZero" -> "Nontrivial";
"LinearOrderedCommGroupWithZero" -> "Inv";
"LinearOrderedCommGroupWithZero" -> "Div";
"LinearOrderedCommGroupWithZero" -> "LinearOrderedCommMonoidWithZero";
"LinearOrderedCommGroupWithZero" -> "CommGroupWithZero";
"LinearOrderedCancelCommMonoid" -> "Ord";
"LinearOrderedCancelCommMonoid" -> "Max";
"LinearOrderedCancelCommMonoid" -> "Min";
"LinearOrderedCancelCommMonoid" -> "LinearOrderedCommMonoid";
"LinearOrderedCancelCommMonoid" -> "OrderedCancelCommMonoid";
"AddSemigroup" -> "Add";
"LinearOrderedSemifield" -> "Inv";
"LinearOrderedSemifield" -> "LinearOrderedCommSemiring";
"LinearOrderedSemifield" -> "Semifield";
"LinearOrderedSemifield" -> "Div";
"LinearOrderedSemifield" -> "DenselyOrdered";
"RightCancelMonoid" -> "Monoid";
"RightCancelMonoid" -> "One";
"RightCancelMonoid" -> "RightCancelSemigroup";
"OrderedCommRing" -> "CommRing";
"OrderedCommRing" -> "OrderedRing";
"OrderedCommRing" -> "OrderedCommSemiring";
"PseudoEMetricSpace" -> "UniformSpace";
"PseudoEMetricSpace" -> "ParacompactSpace";
"PseudoEMetricSpace" -> "EDist";
"NormedStarGroup" -> "ContinuousStar";
"OrderTop" -> "Top";
"InvolutiveInv" -> "Inv";
"EMetricSpace" -> "SeparatedSpace";
"EMetricSpace" -> "PseudoEMetricSpace";
"DivInvMonoid" -> "Monoid";
"DivInvMonoid" -> "Inv";
"DivInvMonoid" -> "Div";
"CircularPartialOrder" -> "CircularPreorder";
"NormedField" -> "NormedCommRing";
"NormedField" -> "Norm";
"NormedField" -> "MetricSpace";
"NormedField" -> "Field";
"NormedField" -> "NormedDivisionRing";
"InvOneClass" -> "One";
"InvOneClass" -> "Inv";
"LeftCancelSemigroup" -> "Semigroup";
"LeftCancelSemigroup" -> "IsLeftCancelMul";
"CompactSpace" -> "ParacompactSpace";
"CompactSpace" -> "WeaklyLocallyCompactSpace";
"CompactSpace" -> "SigmaCompactSpace";
"AddCommMonoid" -> "AddMonoid";
"AddCommMonoid" -> "AddCommSemigroup";
"SimplyConnectedSpace" -> "PathConnectedSpace";
"AddGroupFilterBasis" -> "TopologicalAddGroup";
"IsCoatomistic" -> "IsCoatomic";
"CharZero" -> "Nontrivial";
"CharZero" -> "Infinite";
"Lean.Eval" -> "Lean.MetaEval";
"CategoryTheory.Preadditive" -> "CategoryTheory.Limits.HasZeroMorphisms";
"LinearOrderedCommRing" -> "StrictOrderedCommRing";
"LinearOrderedCommRing" -> "LinearOrderedCommSemiring";
"LinearOrderedCommRing" -> "LinearOrderedRing";
"LinearOrderedCommRing" -> "CommMonoid";
"NormedCommGroup" -> "NormedGroup";
"NormedCommGroup" -> "Norm";
"NormedCommGroup" -> "CommGroup";
"NormedCommGroup" -> "MetricSpace";
"NormedCommGroup" -> "SeminormedCommGroup";
"CommSemiring" -> "CommMonoidWithZero";
"CommSemiring" -> "Semiring";
"CommSemiring" -> "NonUnitalCommSemiring";
"CommSemiring" -> "CommMonoid";
"OmegaCompletePartialOrder" -> "PartialOrder";
"CategoryTheory.Limits.HasStrictInitialObjects" -> "CategoryTheory.Limits.InitialMonoClass";
"AddRightCancelMonoid" -> "AddRightCancelSemigroup";
"AddRightCancelMonoid" -> "AddMonoid";
"AddRightCancelMonoid" -> "Zero";
"CommSemigroup" -> "Semigroup";
"CommSemigroup" -> "IsCommJordan";
"IdemCommSemiring" -> "CommSemiring";
"IdemCommSemiring" -> "IdemSemiring";
"IdemCommSemiring" -> "SemilatticeSup";
"DivisionSemiring" -> "Nontrivial";
"DivisionSemiring" -> "Inv";
"DivisionSemiring" -> "GroupWithZero";
"DivisionSemiring" -> "Div";
"DivisionSemiring" -> "Semiring";
"OrderedCommSemiring" -> "OrderedSemiring";
"OrderedCommSemiring" -> "CommSemiring";
"CategoryTheory.Bicategory" -> "CategoryTheory.CategoryStruct";
"DistribLattice" -> "Lattice";
"DistribLattice" -> "IsModularLattice";
"LieRing" -> "AddCommGroup";
"InvolutiveNeg" -> "Neg";
"PseudoMetricSpace" -> "TopologicalSpace.PseudoMetrizableSpace";
"PseudoMetricSpace" -> "UniformSpace";
"PseudoMetricSpace" -> "NNDist";
"PseudoMetricSpace" -> "PseudoEMetricSpace";
"PseudoMetricSpace" -> "Dist";
"PseudoMetricSpace" -> "EDist";
"PseudoMetricSpace" -> "Bornology";
"AddGroup" -> "SubNegMonoid";
"AddGroup" -> "AddCancelMonoid";
"AddGroup" -> "SubtractionMonoid";
"AddZeroClass" -> "Add";
"AddZeroClass" -> "Zero";
"SemilatticeInf" -> "PartialOrder";
"SemilatticeInf" -> "CategoryTheory.IsCofilteredOrEmpty";
"SemilatticeInf" -> "Inf";
"MeasurableSup₂" -> "MeasurableSup";
"MonoidWithZero" -> "Monoid";
"MonoidWithZero" -> "SemigroupWithZero";
"MonoidWithZero" -> "MulZeroOneClass";
"MonoidWithZero" -> "Zero";
"LeftCancelMonoid" -> "Monoid";
"LeftCancelMonoid" -> "One";
"LeftCancelMonoid" -> "LeftCancelSemigroup";
"SubNegZeroMonoid" -> "SubNegMonoid";
"SubNegZeroMonoid" -> "NegZeroClass";
"NonAssocSemiring" -> "One";
"NonAssocSemiring" -> "AddCommMonoidWithOne";
"NonAssocSemiring" -> "NatCast";
"NonAssocSemiring" -> "MulZeroOneClass";
"NonAssocSemiring" -> "NonUnitalNonAssocSemiring";
"DenselyNormedField" -> "NormedField";
"DenselyNormedField" -> "NontriviallyNormedField";
"AlexandrovDiscrete" -> "TopologicalSpace.FirstCountableTopology";
"AlexandrovDiscrete" -> "LocallyCompactSpace";
"UnitalShelf" -> "One";
"UnitalShelf" -> "Shelf";
"StarOrderedRing" -> "OrderedAddCommMonoid";
"StarOrderedRing" -> "ExistsAddOfLE";
"StarOrderedRing" -> "StarRing";
"Fintype" -> "Finite";
"Fintype" -> "Small";
"AddRightCancelSemigroup" -> "IsRightCancelAdd";
"AddRightCancelSemigroup" -> "AddSemigroup";
"MetricSpace" -> "SeparatedSpace";
"MetricSpace" -> "TopologicalSpace.MetrizableSpace";
"MetricSpace" -> "EMetricSpace";
"MetricSpace" -> "PseudoMetricSpace";
"NonarchimedeanGroup" -> "TopologicalGroup";
"CategoryTheory.EssentiallySmall" -> "CategoryTheory.LocallySmall";
"Order.Coframe" -> "DistribLattice";
"Order.Coframe" -> "CompleteLattice";
"LinearOrderedAddCommMonoidWithTop" -> "LinearOrderedAddCommMonoid";
"LinearOrderedAddCommMonoidWithTop" -> "OrderTop";
"LinearOrderedAddCommMonoidWithTop" -> "Top";
"SubtractionMonoid" -> "SubNegMonoid";
"SubtractionMonoid" -> "InvolutiveNeg";
"SubtractionMonoid" -> "SubNegZeroMonoid";
"LinearOrderedCommMonoidWithZero" -> "ZeroLEOneClass";
"LinearOrderedCommMonoidWithZero" -> "CommMonoidWithZero";
"LinearOrderedCommMonoidWithZero" -> "LinearOrderedCommMonoid";
"LinearOrderedCommMonoidWithZero" -> "Zero";
"CategoryTheory.SymmetricCategory" -> "CategoryTheory.BraidedCategory";
"NonUnitalSemiring" -> "SemigroupWithZero";
"NonUnitalSemiring" -> "NonUnitalNonAssocSemiring";
"CategoryTheory.NormalMonoCategory" -> "CategoryTheory.RegularMonoCategory";
"CanonicallyOrderedAddMonoid" -> "OrderedAddCommMonoid";
"CanonicallyOrderedAddMonoid" -> "OrderBot";
"CanonicallyOrderedAddMonoid" -> "Bot";
"CanonicallyOrderedAddMonoid" -> "ExistsAddOfLE";
"CanonicallyLinearOrderedAddMonoid" -> "Ord";
"CanonicallyLinearOrderedAddMonoid" -> "LinearOrder";
"CanonicallyLinearOrderedAddMonoid" -> "Max";
"CanonicallyLinearOrderedAddMonoid" -> "Min";
"CanonicallyLinearOrderedAddMonoid" -> "CanonicallyOrderedAddMonoid";
"CanonicallyLinearOrderedAddMonoid" -> "SemilatticeSup";
"StarRing" -> "StarMul";
"StarRing" -> "StarAddMonoid";
"CommMonoidWithZero" -> "MonoidWithZero";
"CommMonoidWithZero" -> "CommMonoid";
"CommMonoidWithZero" -> "Zero";
"StrongRankCondition" -> "RankCondition";
"GeneralizedBooleanAlgebra" -> "GeneralizedCoheytingAlgebra";
"GeneralizedBooleanAlgebra" -> "OrderBot";
"GeneralizedBooleanAlgebra" -> "Bot";
"GeneralizedBooleanAlgebra" -> "DistribLattice";
"GeneralizedBooleanAlgebra" -> "SDiff";
"T2Space" -> "QuasiSober";
"T2Space" -> "T1Space";
"T2Space" -> "QuasiSeparatedSpace";
"EuclideanDomain" -> "Mod";
"EuclideanDomain" -> "Nontrivial";
"EuclideanDomain" -> "IsDomain";
"EuclideanDomain" -> "CommRing";
"EuclideanDomain" -> "Div";
"EuclideanDomain" -> "NoZeroDivisors";
"EuclideanDomain" -> "IsPrincipalIdealRing";
"OrderedCancelAddCommMonoid" -> "OrderedAddCommMonoid";
"OrderedCancelAddCommMonoid" -> "AddCancelCommMonoid";
"OrderedCancelAddCommMonoid" -> "PartialOrder";
"OrderedCancelAddCommMonoid" -> "AddCommMonoid";
"TotallySeparatedSpace" -> "TotallyDisconnectedSpace";
"Distrib" -> "Mul";
"Distrib" -> "LeftDistribClass";
"Distrib" -> "Add";
"Distrib" -> "RightDistribClass";
"LinearOrderedAddCommGroup" -> "LinearOrderedCancelAddCommMonoid";
"LinearOrderedAddCommGroup" -> "Ord";
"LinearOrderedAddCommGroup" -> "LinearOrder";
"LinearOrderedAddCommGroup" -> "Max";
"LinearOrderedAddCommGroup" -> "Min";
"LinearOrderedAddCommGroup" -> "OrderedAddCommGroup";
"MeasurableDiv₂" -> "MeasurableDiv";
"CommGroupWithZero" -> "Nontrivial";
"CommGroupWithZero" -> "Inv";
"CommGroupWithZero" -> "CancelCommMonoidWithZero";
"CommGroupWithZero" -> "DivisionCommMonoid";
"CommGroupWithZero" -> "GroupWithZero";
"CommGroupWithZero" -> "Div";
"CommGroupWithZero" -> "CommMonoidWithZero";
"ToString" -> "Std.ToFormat";
"ToString" -> "Lean.Eval";
"AddMonoid" -> "AddSemigroup";
"AddMonoid" -> "AddZeroClass";
"AddMonoid" -> "Zero";
"T5Space" -> "T4Space";
"T5Space" -> "T1Space";
"CategoryTheory.Limits.HasZeroObject" -> "CategoryTheory.Limits.InitialMonoClass";
"NormedLinearOrderedAddGroup" -> "Norm";
"NormedLinearOrderedAddGroup" -> "MetricSpace";
"NormedLinearOrderedAddGroup" -> "LinearOrderedAddCommGroup";
"NormedLinearOrderedAddGroup" -> "NormedOrderedAddGroup";
"IsCancelAdd" -> "IsRightCancelAdd";
"IsCancelAdd" -> "IsLeftCancelAdd";
"CategoryTheory.Adhesive" -> "CategoryTheory.RegularMonoCategory";
"LinearOrderedCommMonoid" -> "OrderedCommMonoid";
"LinearOrderedCommMonoid" -> "LinearOrder";
"LinearOrderedCommMonoid" -> "CommMonoid";
"CategoryTheory.RigidCategory" -> "CategoryTheory.RightRigidCategory";
"CategoryTheory.RigidCategory" -> "CategoryTheory.LeftRigidCategory";
"TopologicalSpace.SecondCountableTopology" -> "TopologicalSpace.FirstCountableTopology";
"TopologicalSpace.SecondCountableTopology" -> "TopologicalSpace.SeparableSpace";
"MeasurableAdd₂" -> "MeasurableAdd";
"CancelMonoid" -> "IsCancelMul";
"CancelMonoid" -> "RightCancelMonoid";
"CancelMonoid" -> "LeftCancelMonoid";
"CategoryTheory.IsConnected" -> "CategoryTheory.IsPreconnected";
"CategoryTheory.IsConnected" -> "Nonempty";
"IsAlgClosed" -> "Infinite";
"PolishSpace" -> "T2Space";
"PolishSpace" -> "TopologicalSpace.SecondCountableTopology";
"Primcodable" -> "Encodable";
"HasDistribNeg" -> "InvolutiveNeg";
"IsDedekindDomain" -> "IsDomain";
"IsDedekindDomain" -> "IsDedekindRing";
"Semiring" -> "One";
"Semiring" -> "NatCast";
"Semiring" -> "MonoidWithZero";
"Semiring" -> "NonAssocSemiring";
"Semiring" -> "NonUnitalSemiring";
"StarAddMonoid" -> "InvolutiveStar";
"NontriviallyNormedField" -> "NormedField";
"NontriviallyNormedField" -> "NoncompactSpace";
"Countable" -> "Small";
"HenselianLocalRing" -> "LocalRing";
"CompleteLinearOrder" -> "LinearOrder";
"CompleteLinearOrder" -> "ConditionallyCompleteLinearOrderBot";
"CompleteLinearOrder" -> "CompletelyDistribLattice";
"CompleteLinearOrder" -> "CompleteLattice";
"Inhabited" -> "Nonempty";
"CategoryTheory.IsFiltered" -> "CategoryTheory.IsFilteredOrEmpty";
"Subsingleton" -> "Finite";
"Subsingleton" -> "Countable";
"Subsingleton" -> "Small";
"TopologicalSpace.NoetherianSpace" -> "CompactSpace";
"TopologicalSpace.NoetherianSpace" -> "QuasiSeparatedSpace";
"FinEnum" -> "Fintype";
"CompleteSemilatticeInf" -> "PartialOrder";
"CompleteSemilatticeInf" -> "InfSet";
"IsModularLattice" -> "IsLowerModularLattice";
"IsModularLattice" -> "IsUpperModularLattice";
"AddGroupWithOne" -> "IntCast";
"AddGroupWithOne" -> "Neg";
"AddGroupWithOne" -> "AddGroup";
"AddGroupWithOne" -> "AddMonoidWithOne";
"AddGroupWithOne" -> "Sub";
"CategoryTheory.CategoryStruct" -> "Quiver";
"StrictOrderedRing" -> "Nontrivial";
"StrictOrderedRing" -> "StrictOrderedSemiring";
"StrictOrderedRing" -> "OrderedRing";
"StrictOrderedRing" -> "PartialOrder";
"StrictOrderedRing" -> "OrderedAddCommGroup";
"StrictOrderedRing" -> "Ring";
"TwoUniqueSums" -> "UniqueSums";
"DivisionRing" -> "Nontrivial";
"DivisionRing" -> "IsDomain";
"DivisionRing" -> "Inv";
"DivisionRing" -> "OfScientific";
"DivisionRing" -> "Div";
"DivisionRing" -> "DivInvMonoid";
"DivisionRing" -> "DivisionSemiring";
"DivisionRing" -> "RatCast";
"DivisionRing" -> "IsPrincipalIdealRing";
"DivisionRing" -> "Ring";
"T4Space" -> "NormalSpace";
"T4Space" -> "T1Space";
"T4Space" -> "T3Space";
"IrreducibleSpace" -> "Nonempty";
"IrreducibleSpace" -> "ConnectedSpace";
"IrreducibleSpace" -> "PreirreducibleSpace";
"OrderClosedTopology" -> "ClosedIciTopology";
"OrderClosedTopology" -> "ClosedIicTopology";
"Quiver.HasInvolutiveReverse" -> "Quiver.HasReverse";
"NormedOrderedAddGroup" -> "Norm";
"NormedOrderedAddGroup" -> "MetricSpace";
"NormedOrderedAddGroup" -> "OrderedAddCommGroup";
"NormedOrderedAddGroup" -> "NormedAddCommGroup";
"Infinite" -> "Nontrivial";
"SizeOf" -> "WellFoundedRelation";
"CstarRing" -> "NormedStarGroup";
"NormedOrderedGroup" -> "OrderedCommGroup";
"NormedOrderedGroup" -> "Norm";
"NormedOrderedGroup" -> "NormedCommGroup";
"NormedOrderedGroup" -> "MetricSpace";
"IsSimpleAddGroup" -> "Nontrivial";
"Group.IsNilpotent" -> "IsSolvable";
"NonUnitalRing" -> "NonUnitalNonAssocRing";
"NonUnitalRing" -> "NonUnitalSemiring";
"NonUnitalCommSemiring" -> "CommSemigroup";
"NonUnitalCommSemiring" -> "NonUnitalSemiring";
"HeytingAlgebra" -> "HasCompl";
"HeytingAlgebra" -> "Bot";
"HeytingAlgebra" -> "BoundedOrder";
"HeytingAlgebra" -> "GeneralizedHeytingAlgebra";
"NormedLinearOrderedGroup" -> "LinearOrderedCommGroup";
"NormedLinearOrderedGroup" -> "Norm";
"NormedLinearOrderedGroup" -> "MetricSpace";
"NormedLinearOrderedGroup" -> "NormedOrderedGroup";
"ConditionallyCompleteLinearOrder" -> "LinearOrder";
"ConditionallyCompleteLinearOrder" -> "ConditionallyCompleteLattice";
"Order.Frame" -> "DistribLattice";
"Order.Frame" -> "CompleteLattice";
"TwoUniqueProds" -> "UniqueProds";
"AddCommSemigroup" -> "AddSemigroup";
"ValuationRing" -> "IsBezout";
"ValuationRing" -> "LocalRing";
"T1Space" -> "T0Space";
"SeminormedCommGroup" -> "TopologicalGroup";
"SeminormedCommGroup" -> "SeminormedGroup";
"SeminormedCommGroup" -> "LipschitzMul";
"SeminormedCommGroup" -> "UniformGroup";
"SeminormedCommGroup" -> "Norm";
"SeminormedCommGroup" -> "CommGroup";
"SeminormedCommGroup" -> "PseudoMetricSpace";
"IsAtomistic" -> "IsAtomic";
"MulOneClass" -> "One";
"MulOneClass" -> "Mul";
"SubtractionCommMonoid" -> "AddCommMonoid";
"SubtractionCommMonoid" -> "SubtractionMonoid";
"Denumerable" -> "Primcodable";
"Denumerable" -> "Infinite";
"Denumerable" -> "Encodable";
"RightCancelSemigroup" -> "Semigroup";
"RightCancelSemigroup" -> "IsRightCancelMul";
"NonUnitalNonAssocSemiring" -> "Mul";
"NonUnitalNonAssocSemiring" -> "MulZeroClass";
"NonUnitalNonAssocSemiring" -> "AddCommMonoid";
"NonUnitalNonAssocSemiring" -> "Distrib";
"BoundedOrder" -> "OrderBot";
"BoundedOrder" -> "OrderTop";
"NegZeroClass" -> "Neg";
"NegZeroClass" -> "Zero";
"OrderedAddCommGroup" -> "PartialOrder";
"OrderedAddCommGroup" -> "AddCommGroup";
"OrderedAddCommGroup" -> "OrderedCancelAddCommMonoid";
"StrictOrderedCommSemiring" -> "StrictOrderedSemiring";
"StrictOrderedCommSemiring" -> "CommSemiring";
"StrictOrderedCommSemiring" -> "OrderedCommSemiring";
"CompleteLattice" -> "Lattice";
"CompleteLattice" -> "CompleteSemilatticeSup";
"CompleteLattice" -> "ConditionallyCompleteLattice";
"CompleteLattice" -> "InfSet";
"CompleteLattice" -> "SupSet";
"CompleteLattice" -> "Bot";
"CompleteLattice" -> "OmegaCompletePartialOrder";
"CompleteLattice" -> "CompleteSemilatticeInf";
"CompleteLattice" -> "BoundedOrder";
"CompleteLattice" -> "Top";
"CompleteLattice" -> "CompletePartialOrder";
"T3Space" -> "RegularSpace";
"T3Space" -> "T0Space";
"T3Space" -> "T25Space";
"FloorRing" -> "FloorSemiring";
"CategoryTheory.SplitEpiCategory" -> "CategoryTheory.RegularEpiCategory";
"TopologicalRing" -> "ContinuousNeg";
"TopologicalRing" -> "TopologicalAddGroup";
"TopologicalRing" -> "TopologicalSemiring";
"LocallyCompactSpace" -> "WeaklyLocallyCompactSpace";
"ConnectedSpace" -> "PreconnectedSpace";
"ConnectedSpace" -> "Nonempty";
"TopologicalAddGroup" -> "RegularSpace";
"TopologicalAddGroup" -> "HSpace";
"TopologicalAddGroup" -> "ContinuousSub";
"TopologicalAddGroup" -> "ContinuousNeg";
"TopologicalAddGroup" -> "ContinuousAdd";
"Repr" -> "ReprTuple";
"Repr" -> "Lean.Eval";
"IsDedekindRing" -> "IsIntegrallyClosed";
"IsDedekindRing" -> "Ring.DimensionLEOne";
"OrderedCancelCommMonoid" -> "OrderedCommMonoid";
"OrderedCancelCommMonoid" -> "PartialOrder";
"OrderedCancelCommMonoid" -> "CommMonoid";
"OrderedCancelCommMonoid" -> "CancelCommMonoid";
"CategoryTheory.NormalEpiCategory" -> "CategoryTheory.RegularEpiCategory";
"LinearOrderedSemiring" -> "StrictOrderedSemiring";
"LinearOrderedSemiring" -> "Ord";
"LinearOrderedSemiring" -> "Max";
"LinearOrderedSemiring" -> "LinearOrderedAddCommMonoid";
"LinearOrderedSemiring" -> "Min";
"IdemSemiring" -> "OrderBot";
"IdemSemiring" -> "CanonicallyOrderedAddMonoid";
"IdemSemiring" -> "Semiring";
"IdemSemiring" -> "SemilatticeSup";
"CommMonoid" -> "Monoid";
"CommMonoid" -> "CommSemigroup";
"SemilatticeSup" -> "PartialOrder";
"SemilatticeSup" -> "Sup";
"SemilatticeSup" -> "CategoryTheory.IsFilteredOrEmpty";
"CategoryTheory.Limits.HasFiniteColimits" -> "CategoryTheory.Limits.HasFiniteCoproducts";
"Field" -> "Nontrivial";
"Field" -> "IsDomain";
"Field" -> "CommRing";
"Field" -> "Inv";
"Field" -> "Semifield";
"Field" -> "Div";
"Field" -> "LocalRing";
"Field" -> "RatCast";
"Field" -> "EuclideanDomain";
"Field" -> "HenselianLocalRing";
"Field" -> "DivisionRing";
"Field" -> "ValuationRing";
"Field" -> "Ideal.IsJacobson";
"CategoryTheory.StrongMonoCategory" -> "CategoryTheory.Balanced";
"Ring" -> "IntCast";
"Ring" -> "AddCommGroup";
"Ring" -> "NonAssocRing";
"Ring" -> "LieRing";
"Ring" -> "Neg";
"Ring" -> "Semiring";
"Ring" -> "AddGroupWithOne";
"Ring" -> "NonUnitalRing";
"Ring" -> "Sub";
"T25Space" -> "T2Space";
"NumberField" -> "CharZero";
"NonarchimedeanRing" -> "NonarchimedeanAddGroup";
"NonarchimedeanRing" -> "TopologicalRing";
"GeneralizedHeytingAlgebra" -> "Lattice";
"GeneralizedHeytingAlgebra" -> "HImp";
"GeneralizedHeytingAlgebra" -> "OrderTop";
"GeneralizedHeytingAlgebra" -> "DistribLattice";
"GeneralizedHeytingAlgebra" -> "Top";
"MeasureTheory.MeasureSpace" -> "MeasurableSpace";
"NormedRing" -> "Norm";
"NormedRing" -> "NonUnitalNormedRing";
"NormedRing" -> "MetricSpace";
"NormedRing" -> "Ring";
"NormedRing" -> "SeminormedRing";
"CanonicallyOrderedCommSemiring" -> "OrderedCommMonoid";
"CanonicallyOrderedCommSemiring" -> "One";
"CanonicallyOrderedCommSemiring" -> "Mul";
"CanonicallyOrderedCommSemiring" -> "NatCast";
"CanonicallyOrderedCommSemiring" -> "CommSemiring";
"CanonicallyOrderedCommSemiring" -> "OrderedCommSemiring";
"CanonicallyOrderedCommSemiring" -> "NoZeroDivisors";
"CanonicallyOrderedCommSemiring" -> "CanonicallyOrderedAddMonoid";
"CategoryTheory.Limits.HasStrongEpiImages" -> "CategoryTheory.Limits.HasImageMaps";
"Top" -> "Nonempty";
"SeminormedRing" -> "NonUnitalSeminormedRing";
"SeminormedRing" -> "Norm";
"SeminormedRing" -> "PseudoMetricSpace";
"SeminormedRing" -> "Ring";
"NormedDivisionRing" -> "NormOneClass";
"NormedDivisionRing" -> "TopologicalDivisionRing";
"NormedDivisionRing" -> "HasContinuousInv₀";
"NormedDivisionRing" -> "Norm";
"NormedDivisionRing" -> "MetricSpace";
"NormedDivisionRing" -> "DivisionRing";
"NormedDivisionRing" -> "NormedRing";
"CancelMonoidWithZero" -> "IsCancelMulZero";
"CancelMonoidWithZero" -> "MonoidWithZero";
"CancelMonoidWithZero" -> "NoZeroDivisors";
"LinearOrderedField" -> "Inv";
"LinearOrderedField" -> "Div";
"LinearOrderedField" -> "LinearOrderedSemifield";
"LinearOrderedField" -> "LinearOrderedCommRing";
"LinearOrderedField" -> "RatCast";
"LinearOrderedField" -> "Field";
"TopologicalSemiring" -> "ContinuousMul";
"TopologicalSemiring" -> "ContinuousAdd";
"Encodable" -> "Countable";
"CircularOrder" -> "CircularPartialOrder";
"MeasurableMul₂" -> "MeasurableMul";
"Preorder" -> "Topology.IsUpperSet";
"Preorder" -> "Topology.IsLowerSet";
"Preorder" -> "LE";
"Preorder" -> "LT";
"BooleanRing" -> "CommRing";
"BooleanRing" -> "Ring";
"CategoryTheory.StrongEpiCategory" -> "CategoryTheory.Balanced";
"NormedAddCommGroup" -> "SeminormedAddCommGroup";
"NormedAddCommGroup" -> "AddCommGroup";
"NormedAddCommGroup" -> "Norm";
"NormedAddCommGroup" -> "MetricSpace";
"NormedAddCommGroup" -> "NormedAddGroup";
"AddMonoidWithOne" -> "One";
"AddMonoidWithOne" -> "NatCast";
"AddMonoidWithOne" -> "AddMonoid";
"PathConnectedSpace" -> "ConnectedSpace";
"CategoryTheory.Category" -> "CategoryTheory.CategoryStruct";
"PreirreducibleSpace" -> "PreconnectedSpace";
"CanonicallyLinearOrderedMonoid" -> "Ord";
"CanonicallyLinearOrderedMonoid" -> "LinearOrder";
"CanonicallyLinearOrderedMonoid" -> "Max";
"CanonicallyLinearOrderedMonoid" -> "CanonicallyOrderedMonoid";
"CanonicallyLinearOrderedMonoid" -> "Min";
"CanonicallyLinearOrderedMonoid" -> "SemilatticeSup";
"FrechetUrysohnSpace" -> "SequentialSpace";
"NormedAddGroup" -> "SeminormedAddGroup";
"NormedAddGroup" -> "Norm";
"NormedAddGroup" -> "AddGroup";
"NormedAddGroup" -> "MetricSpace";
"CancelCommMonoid" -> "LeftCancelMonoid";
"CancelCommMonoid" -> "CancelMonoid";
"CancelCommMonoid" -> "CommMonoid";
"Zero" -> "Nonempty";
"UniformAddGroup" -> "TopologicalAddGroup";
"AlexandrovDiscreteSpace" -> "TopologicalSpace";
"AlexandrovDiscreteSpace" -> "AlexandrovDiscrete";
"CompletePartialOrder" -> "PartialOrder";
"CompletePartialOrder" -> "SupSet";
"CompletePartialOrder" -> "OmegaCompletePartialOrder";
"SeparatedSpace" -> "UniformSpace" [style=dashed];
"TopologicalSpace.PseudoMetrizableSpace" -> "TopologicalSpace" [style=dashed];
"PerfectField" -> "Field" [style=dashed];
"CategoryTheory.IsPreconnected" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.InitiallySmall" -> "CategoryTheory.Category" [style=dashed];
"NormOneClass" -> "One" [style=dashed];
"NormOneClass" -> "Norm" [style=dashed];
"CategoryTheory.RegularMonoCategory" -> "CategoryTheory.Category" [style=dashed];
"MeasurableInf₂" -> "MeasurableSpace" [style=dashed];
"MeasurableInf₂" -> "Inf" [style=dashed];
"NonarchimedeanAddGroup" -> "TopologicalSpace" [style=dashed];
"NonarchimedeanAddGroup" -> "AddGroup" [style=dashed];
"CategoryTheory.Limits.HasZeroMorphisms" -> "CategoryTheory.Category" [style=dashed];
"CategoryTheory.IsIdempotentComplete" -> "CategoryTheory.Category" [style=dashed];
"IsDomain" -> "Semiring" [style=dashed];
"IsRightCancelAdd" -> "Add" [style=dashed];
"ExistsMulOfLE" -> "Mul" [style=dashed];
"ExistsMulOfLE" -> "LE" [style=dashed];
"AddMonoid.FG" -> "AddMonoid" [style=dashed];
"StandardBorelSpace" -> "MeasurableSpace" [style=dashed];
"OrderTopology" -> "TopologicalSpace" [style=dashed];
"OrderTopology" -> "Preorder" [style=dashed];
"LipschitzAdd" -> "PseudoMetricSpace" [style=dashed];
"LipschitzAdd" -> "AddMonoid" [style=dashed];
"CategoryTheory.Preregular" -> "CategoryTheory.Category" [style=dashed];
"TopologicalDivisionRing" -> "TopologicalSpace" [style=dashed];
"TopologicalDivisionRing" -> "DivisionRing" [style=dashed];
"CategoryTheory.Noetherian" -> "CategoryTheory.Category" [style=dashed];
"HasUpperLowerClosure" -> "TopologicalSpace" [style=dashed];
"HasUpperLowerClosure" -> "Preorder" [style=dashed];
"CompleteSpace" -> "UniformSpace" [style=dashed];
"IsSolvable" -> "Group" [style=dashed];
"TopologicalSpace.MetrizableSpace" -> "TopologicalSpace" [style=dashed];
"IsFreeGroupoid" -> "CategoryTheory.Groupoid" [style=dashed];
"GCDMonoid" -> "CancelCommMonoidWithZero" [style=dashed];
"LocallyFiniteOrderTop" -> "Preorder" [style=dashed];
"CategoryTheory.RegularEpiCategory" -> "CategoryTheory.Category" [style=dashed];
"TopologicalGroup" -> "Group" [style=dashed];
"TopologicalGroup" -> "TopologicalSpace" [style=dashed];
"Quiver.Arborescence" -> "Quiver" [style=dashed];
"CategoryTheory.Limits.HasFiniteWidePullbacks" -> "CategoryTheory.Category" [style=dashed];
"ClosedIciTopology" -> "TopologicalSpace" [style=dashed];
"ClosedIciTopology" -> "Preorder" [style=dashed];
"CategoryTheory.Limits.HasImages" -> "CategoryTheory.Category" [style=dashed];
"RegularSpace" -> "TopologicalSpace" [style=dashed];
"TopologicalSpace.FirstCountableTopology" -> "TopologicalSpace" [style=dashed];
"CategoryTheory.IsCofiltered" -> "CategoryTheory.Category" [style=dashed];