-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathfoundational_types.html
6346 lines (5532 loc) · 317 KB
/
foundational_types.html
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
<!DOCTYPE html>
<html lang="en">
<head>
<link rel="stylesheet" href="https://pygae.github.io/lean-ga-docs/style.css">
<link rel="stylesheet" href="https://pygae.github.io/lean-ga-docs/pygments.css">
<link rel="stylesheet" href="https://pygae.github.io/lean-ga-docs/pygments-dark.css">
<link rel="shortcut icon" href="https://pygae.github.io/lean-ga-docs/favicon.ico">
<title>foundational types - mathlib3 docs</title>
<meta charset="UTF-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<meta name="description" content="The Lean 3 mathematical library, mathlib, is a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant." />
<link rel="canonical" href="https://leanprover-community.github.io/mathlib_docs/attributes.html" />
<meta property="og:title" content="foundational types - mathlib3 docs">
<meta property="og:site_name" content="mathlib for Lean 3 - API documentation">
<meta property="og:description" content="The Lean 3 mathematical library, mathlib, is a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant.">
<meta property="og:image" content="https://pygae.github.io/lean-ga-docs/meta-og.png">
<meta name="twitter:card" content="summary">
<script src="https://pygae.github.io/lean-ga-docs/color_scheme.js"></script>
</head>
<body>
<input id="nav_toggle" type="checkbox">
<header>
<h1><label for="nav_toggle"></label><a href="https://leanprover-community.github.io/lean3">mathlib3</a>
<span>documentation</span></h1>
<p class="header_filename break_within">foundational types</p>
<form action="https://google.com/search" method="get" id="search_form">
<input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib_docs">
<input type="text" name="q" autocomplete="off">
<button>Google site search</button>
</form>
</header>
<nav class="internal_nav">
<h3><a href="#top">foundational types</a></h3>
</nav>
<main>
<a id="top"></a>
<div class="docfile">
<h1>foundational types</h1>
<p>Some of Lean's types are not defined in any Lean source files (even the <code>prelude</code>) since they come from its foundational type theory. This page provides basic documentation for these types.</p>
<p>For a more in-depth explanation of Lean's type theory, refer to
<a href="https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html">TPiL</a>.</p>
<h2 id="codesort-ucode" class="markdown-heading"><code>Sort u</code> <a class="hover-link" href="#codesort-ucode">#</a></h2>
<p><code>Sort u</code> is the type of types in Lean, and <code>Sort u : Sort (u + 1)</code>.</p>
<details class="instances-for">
<summary>Instances for <code><span class="name">Sort u</span></code></summary>
<ul>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/basic.html#sort.inhabited">sort.inhabited</a></li>
</ul>
</details>
<h2 id="codetype-ucode" class="markdown-heading"><code>Type u</code> <a class="hover-link" href="#codetype-ucode">#</a></h2>
<p><code>Type u</code> is notation for <code>Sort (u + 1)</code>.</p>
<details class="instances-for">
<summary>Instances for <code><span class="name">Type u</span></code></summary>
<ul>
<li><a href="https://pygae.github.io/lean-ga-docs/data/set_like/basic.html#set_like.has_coe_to_sort">set_like.has_coe_to_sort</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/set/basic.html#set.has_coe_to_sort">set.has_coe_to_sort</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/finset/basic.html#finset.has_coe_to_sort">finset.has_coe_to_sort</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/set_theory/cardinal/basic.html#cardinal.is_equivalent">cardinal.is_equivalent</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/set_theory/cardinal/basic.html#cardinal.can_lift_cardinal_Type">cardinal.can_lift_cardinal_Type</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/combinatorics/quiver/subquiver.html#wide_subquiver_has_coe_to_sort">wide_subquiver_has_coe_to_sort</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/category_theory/types.html#category_theory.types">category_theory.types</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/category_theory/types.html#category_theory.sort.split_epi_category">category_theory.sort.split_epi_category</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/category_theory/concrete_category/bundled.html#category_theory.bundled.has_coe_to_sort">category_theory.bundled.has_coe_to_sort</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/category_theory/category/Cat.html#category_theory.Cat.has_coe_to_sort">category_theory.Cat.has_coe_to_sort</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/category_theory/concrete_category/basic.html#category_theory.concrete_category.types">category_theory.concrete_category.types</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/category/Mon/basic.html#Mon.has_coe_to_sort">Mon.has_coe_to_sort</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/category/Mon/basic.html#AddMon.has_coe_to_sort">AddMon.has_coe_to_sort</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/category/Mon/basic.html#CommMon.has_coe_to_sort">CommMon.has_coe_to_sort</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/category/Mon/basic.html#AddCommMon.has_coe_to_sort">AddCommMon.has_coe_to_sort</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/category/Group/basic.html#Group.has_coe_to_sort">Group.has_coe_to_sort</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/category/Group/basic.html#AddGroup.has_coe_to_sort">AddGroup.has_coe_to_sort</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/category/Group/basic.html#CommGroup.has_coe_to_sort">CommGroup.has_coe_to_sort</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/category/Group/basic.html#AddCommGroup.has_coe_to_sort">AddCommGroup.has_coe_to_sort</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/category/Ring/basic.html#SemiRing.has_coe_to_sort">SemiRing.has_coe_to_sort</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/category/Ring/basic.html#Ring.has_coe_to_sort">Ring.has_coe_to_sort</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/category/Ring/basic.html#CommSemiRing.has_coe_to_sort">CommSemiRing.has_coe_to_sort</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/category/Ring/basic.html#CommRing.has_coe_to_sort">CommRing.has_coe_to_sort</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/category/Module/basic.html#Module.has_coe_to_sort">Module.has_coe_to_sort</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/category/Algebra/basic.html#Algebra.has_coe_to_sort">Algebra.has_coe_to_sort</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/geometric_algebra/from_mathlib/category_theory.html#QuadraticModule.has_coe_to_sort">QuadraticModule.has_coe_to_sort</a></li>
</ul>
</details>
<h2 id="codepropcode" class="markdown-heading"><code>Prop</code> <a class="hover-link" href="#codepropcode">#</a></h2>
<p><code>Prop</code> is notation for <code>Sort 0</code>.</p>
<details class="instances-for">
<summary>Instances for <code><span class="name">Prop</span></code></summary>
<ul>
<li><a href="https://pygae.github.io/lean-ga-docs/init/algebra/classes.html#is_symm_op_of_is_symm">is_symm_op_of_is_symm</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/logic.html#prop.inhabited">prop.inhabited</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/coe.html#coe_bool_to_Prop">coe_bool_to_Prop</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/coe.html#coe_sort_bool">coe_sort_bool</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/basic.html#iff.is_refl">iff.is_refl</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/basic.html#iff.is_trans">iff.is_trans</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/basic.html#xor.is_commutative">xor.is_commutative</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/nontrivial.html#sort.nontrivial">sort.nontrivial</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/basic.html#Prop.has_compl">Prop.has_compl</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/basic.html#Prop.has_le">Prop.has_le</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/basic.html#Prop.partial_order">Prop.partial_order</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/prop_instances.html#Prop.distrib_lattice">Prop.distrib_lattice</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/prop_instances.html#Prop.bounded_order">Prop.bounded_order</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/prop_instances.html#Prop.le_is_total">Prop.le_is_total</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/prop_instances.html#Prop.linear_order">Prop.linear_order</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/heyting/basic.html#Prop.heyting_algebra">Prop.heyting_algebra</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/boolean_algebra.html#Prop.boolean_algebra">Prop.boolean_algebra</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/complete_lattice.html#Prop.complete_lattice">Prop.complete_lattice</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/complete_lattice.html#Prop.complete_linear_order">Prop.complete_linear_order</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/complete_boolean_algebra.html#Prop.complete_boolean_algebra">Prop.complete_boolean_algebra</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/fintype/basic.html#Prop.fintype">Prop.fintype</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/countable/defs.html#Prop.countable'">Prop.countable'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/encodable/basic.html#Prop.encodable">Prop.encodable</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/order.html#sierpinski_space">sierpinski_space</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/tactic/has_variable_names.html#Prop.has_variable_names">Prop.has_variable_names</a></li>
</ul>
</details>
<h2 id="pi-types-codeπ-a--α-β-acode" class="markdown-heading">Pi types, <code>Π a : α, β a</code> <a class="hover-link" href="#pi-types-codeπ-a--α-β-acode">#</a></h2>
<p>The type of dependent functions is known as a pi type.
Non-dependent functions and implications are a special case.</p>
<p>Note that these can also be written with the alternative notations:</p>
<ul>
<li><code>∀ a : α, β a</code>, conventionally used where <code>β a : Prop</code>.</li>
<li><code>α → γ</code>, possible only if <code>β a = γ</code> for all <code>a</code>.</li>
</ul>
<p>Lean also permits ASCII-only spellings of the three variants:</p>
<ul>
<li><code>Pi a : A, B a</code> for <code>Π a : α, β a</code></li>
<li><code>forall a : A, B a</code> for <code>∀ a : α, β a</code></li>
<li><code>A -> B</code>, for <code>α → β</code></li>
</ul>
<p>Note that despite not itself being a function, <code>(→)</code> is available as infix notation for
<code>λ α β, α → β</code>.</p>
<details class="instances-for">
<summary>Instances for <code><span class="name">Π a : α, β a</span></code></summary>
<ul>
<li><a href="https://pygae.github.io/lean-ga-docs/data/fun_like/basic.html#fun_like.has_coe_to_fun">fun_like.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/logic.html#pi.inhabited">pi.inhabited</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/funext.html#pi.subsingleton">pi.subsingleton</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/coe.html#lift_pi_range">lift_pi_range</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/nonempty.html#pi.nonempty">pi.nonempty</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/tactic/lift.html#pi.can_lift">pi.can_lift</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/tactic/lift.html#pi_subtype.can_lift">pi_subtype.can_lift</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/control/traversable/basic.html#applicative_transformation.has_coe_to_fun">applicative_transformation.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/quot.html#pi_setoid">pi_setoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/is_empty.html#pi.is_empty">pi.is_empty</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/unique.html#pi.unique">pi.unique</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/unique.html#pi.unique_of_is_empty">pi.unique_of_is_empty</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/nontrivial.html#pi.nontrivial">pi.nontrivial</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/basic.html#pi.has_compl">pi.has_compl</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/basic.html#pi.has_le">pi.has_le</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/basic.html#pi.preorder">pi.preorder</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/basic.html#pi.partial_order">pi.partial_order</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/basic.html#pi.has_sdiff">pi.has_sdiff</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/basic.html#pi.densely_ordered">pi.densely_ordered</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/max.html#pi.no_max_order">pi.no_max_order</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/max.html#pi.no_min_order">pi.no_min_order</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/pi/algebra.html#pi.has_one">pi.has_one</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/pi/algebra.html#pi.has_zero">pi.has_zero</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/pi/algebra.html#pi.has_mul">pi.has_mul</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/pi/algebra.html#pi.has_add">pi.has_add</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/pi/algebra.html#pi.has_smul">pi.has_smul</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/pi/algebra.html#pi.has_vadd">pi.has_vadd</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/pi/algebra.html#pi.has_pow">pi.has_pow</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/pi/algebra.html#pi.has_inv">pi.has_inv</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/pi/algebra.html#pi.has_neg">pi.has_neg</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/pi/algebra.html#pi.has_div">pi.has_div</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/pi/algebra.html#pi.has_sub">pi.has_sub</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/lattice.html#pi.has_sup">pi.has_sup</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/lattice.html#pi.has_inf">pi.has_inf</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/lattice.html#pi.semilattice_sup">pi.semilattice_sup</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/lattice.html#pi.semilattice_inf">pi.semilattice_inf</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/lattice.html#pi.lattice">pi.lattice</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/lattice.html#pi.distrib_lattice">pi.distrib_lattice</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/bounded_order.html#pi.has_bot">pi.has_bot</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/bounded_order.html#pi.has_top">pi.has_top</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/bounded_order.html#pi.order_top">pi.order_top</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/bounded_order.html#pi.order_bot">pi.order_bot</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/bounded_order.html#pi.bounded_order">pi.bounded_order</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/heyting/basic.html#pi.has_himp">pi.has_himp</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/heyting/basic.html#pi.has_hnot">pi.has_hnot</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/heyting/basic.html#pi.generalized_heyting_algebra">pi.generalized_heyting_algebra</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/heyting/basic.html#pi.generalized_coheyting_algebra">pi.generalized_coheyting_algebra</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/heyting/basic.html#pi.heyting_algebra">pi.heyting_algebra</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/heyting/basic.html#pi.coheyting_algebra">pi.coheyting_algebra</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/boolean_algebra.html#pi.boolean_algebra">pi.boolean_algebra</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/set/basic.html#set.pi_set_coe.can_lift">set.pi_set_coe.can_lift</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.semigroup">pi.semigroup</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.add_semigroup">pi.add_semigroup</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.semigroup_with_zero">pi.semigroup_with_zero</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.comm_semigroup">pi.comm_semigroup</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.add_comm_semigroup">pi.add_comm_semigroup</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.mul_one_class">pi.mul_one_class</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.add_zero_class">pi.add_zero_class</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.monoid">pi.monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.add_monoid">pi.add_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.comm_monoid">pi.comm_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.add_comm_monoid">pi.add_comm_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.div_inv_monoid">pi.div_inv_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.sub_neg_monoid">pi.sub_neg_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.has_involutive_inv">pi.has_involutive_inv</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.has_involutive_neg">pi.has_involutive_neg</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.division_monoid">pi.division_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.subtraction_monoid">pi.subtraction_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.division_comm_monoid">pi.division_comm_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.subtraction_comm_monoid">pi.subtraction_comm_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.group">pi.group</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.add_group">pi.add_group</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.comm_group">pi.comm_group</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.add_comm_group">pi.add_comm_group</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.left_cancel_semigroup">pi.left_cancel_semigroup</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.add_left_cancel_semigroup">pi.add_left_cancel_semigroup</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.right_cancel_semigroup">pi.right_cancel_semigroup</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.add_right_cancel_semigroup">pi.add_right_cancel_semigroup</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.left_cancel_monoid">pi.left_cancel_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.add_left_cancel_monoid">pi.add_left_cancel_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.right_cancel_monoid">pi.right_cancel_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.add_right_cancel_monoid">pi.add_right_cancel_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.cancel_monoid">pi.cancel_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.add_cancel_monoid">pi.add_cancel_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.cancel_comm_monoid">pi.cancel_comm_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.add_cancel_comm_monoid">pi.add_cancel_comm_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.mul_zero_class">pi.mul_zero_class</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.mul_zero_one_class">pi.mul_zero_one_class</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.monoid_with_zero">pi.monoid_with_zero</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/group/pi.html#pi.comm_monoid_with_zero">pi.comm_monoid_with_zero</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/nat/cast/basic.html#pi.has_nat_cast">pi.has_nat_cast</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/nat/cast/basic.html#pi.add_monoid_with_one">pi.add_monoid_with_one</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/int/cast/lemmas.html#pi.has_int_cast">pi.has_int_cast</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/int/cast/lemmas.html#pi.add_group_with_one">pi.add_group_with_one</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/ring/pi.html#pi.distrib">pi.distrib</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/ring/pi.html#pi.non_unital_non_assoc_semiring">pi.non_unital_non_assoc_semiring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/ring/pi.html#pi.non_unital_semiring">pi.non_unital_semiring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/ring/pi.html#pi.non_assoc_semiring">pi.non_assoc_semiring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/ring/pi.html#pi.semiring">pi.semiring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/ring/pi.html#pi.non_unital_comm_semiring">pi.non_unital_comm_semiring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/ring/pi.html#pi.comm_semiring">pi.comm_semiring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/ring/pi.html#pi.non_unital_non_assoc_ring">pi.non_unital_non_assoc_ring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/ring/pi.html#pi.non_unital_ring">pi.non_unital_ring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/ring/pi.html#pi.non_assoc_ring">pi.non_assoc_ring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/ring/pi.html#pi.ring">pi.ring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/ring/pi.html#pi.non_unital_comm_ring">pi.non_unital_comm_ring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/ring/pi.html#pi.comm_ring">pi.comm_ring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.has_smul'">pi.has_smul'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.has_vadd'">pi.has_vadd'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.is_scalar_tower">pi.is_scalar_tower</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.vadd_assoc_class">pi.vadd_assoc_class</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.is_scalar_tower'">pi.is_scalar_tower'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.vadd_assoc_class'">pi.vadd_assoc_class'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.is_scalar_tower''">pi.is_scalar_tower''</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.vadd_assoc_class''">pi.vadd_assoc_class''</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.smul_comm_class">pi.smul_comm_class</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.vadd_comm_class">pi.vadd_comm_class</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.smul_comm_class'">pi.smul_comm_class'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.vadd_comm_class'">pi.vadd_comm_class'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.smul_comm_class''">pi.smul_comm_class''</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.vadd_comm_class''">pi.vadd_comm_class''</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.is_central_scalar">pi.is_central_scalar</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.is_central_vadd">pi.is_central_vadd</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.has_faithful_smul">pi.has_faithful_smul</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.has_faithful_vadd">pi.has_faithful_vadd</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.mul_action">pi.mul_action</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.add_action">pi.add_action</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.mul_action'">pi.mul_action'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.add_action'">pi.add_action'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.smul_zero_class">pi.smul_zero_class</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.smul_zero_class'">pi.smul_zero_class'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.distrib_smul">pi.distrib_smul</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.distrib_smul'">pi.distrib_smul'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.distrib_mul_action">pi.distrib_mul_action</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.distrib_mul_action'">pi.distrib_mul_action'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.mul_distrib_mul_action">pi.mul_distrib_mul_action</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#pi.mul_distrib_mul_action'">pi.mul_distrib_mul_action'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/module/pi.html#pi.smul_with_zero">pi.smul_with_zero</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/module/pi.html#pi.smul_with_zero'">pi.smul_with_zero'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/module/pi.html#pi.mul_action_with_zero">pi.mul_action_with_zero</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/module/pi.html#pi.mul_action_with_zero'">pi.mul_action_with_zero'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/module/pi.html#pi.module">pi.module</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/module/pi.html#pi.module'">pi.module'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/module/pi.html#pi.no_zero_smul_divisors">pi.no_zero_smul_divisors</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/complete_lattice.html#pi.has_Sup">pi.has_Sup</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/complete_lattice.html#pi.has_Inf">pi.has_Inf</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/complete_lattice.html#pi.complete_lattice">pi.complete_lattice</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/complete_boolean_algebra.html#pi.frame">pi.frame</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/complete_boolean_algebra.html#pi.coframe">pi.coframe</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/complete_boolean_algebra.html#pi.complete_distrib_lattice">pi.complete_distrib_lattice</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/complete_boolean_algebra.html#pi.complete_boolean_algebra">pi.complete_boolean_algebra</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/finset/basic.html#finset.pi_finset_coe.can_lift">finset.pi_finset_coe.can_lift</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/fintype/basic.html#pfun_fintype">pfun_fintype</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/countable/basic.html#pi.countable">pi.countable</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/fintype/prod.html#pi.infinite_of_left">pi.infinite_of_left</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/fintype/prod.html#pi.infinite_of_right">pi.infinite_of_right</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/fintype/pi.html#pi.fintype">pi.fintype</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/finite/basic.html#pi.finite">pi.finite</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/dfinsupp/basic.html#dfinsupp.has_coe_to_fun">dfinsupp.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/conditionally_complete_lattice/basic.html#pi.conditionally_complete_lattice">pi.conditionally_complete_lattice</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/omega_complete_partial_order.html#pi.omega_complete_partial_order">pi.omega_complete_partial_order</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/order/kleene.html#pi.idem_semiring">pi.idem_semiring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/order/kleene.html#pi.idem_comm_semiring">pi.idem_comm_semiring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/order/kleene.html#pi.kleene_algebra">pi.kleene_algebra</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/equiv/list.html#encodable.fin_pi">encodable.fin_pi</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/small/basic.html#small_Pi">small_Pi</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/ring_theory/finiteness.html#module.finite.pi">module.finite.pi</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/direct_sum/basic.html#direct_sum.has_coe_to_fun">direct_sum.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/algebra/pi.html#pi.algebra">pi.algebra</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/star/pi.html#pi.has_star">pi.has_star</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/star/pi.html#pi.has_trivial_star">pi.has_trivial_star</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/star/pi.html#pi.has_involutive_star">pi.has_involutive_star</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/star/pi.html#pi.star_semigroup">pi.star_semigroup</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/star/pi.html#pi.star_add_monoid">pi.star_add_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/star/pi.html#pi.star_ring">pi.star_ring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/star/pi.html#pi.star_module">pi.star_module</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/linear_algebra/free_module/basic.html#module.free.pi">module.free.pi</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/ring_theory/noetherian.html#is_noetherian_pi">is_noetherian_pi</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/linear_algebra/finite_dimensional.html#finite_dimensional.finite_dimensional_pi'">finite_dimensional.finite_dimensional_pi'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/constructions.html#Pi.topological_space">Pi.topological_space</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/constructions.html#Pi.discrete_topology">Pi.discrete_topology</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/bases.html#topological_space.pi.first_countable_topology">topological_space.pi.first_countable_topology</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/bases.html#topological_space.pi.second_countable_topology">topological_space.pi.second_countable_topology</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/subset_properties.html#pi.compact_space">pi.compact_space</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/subset_properties.html#pi.locally_compact_space_of_finite">pi.locally_compact_space_of_finite</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/subset_properties.html#pi.locally_compact_space">pi.locally_compact_space</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/subset_properties.html#pi.sigma_compact_space">pi.sigma_compact_space</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/connected.html#pi.preconnected_space">pi.preconnected_space</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/connected.html#pi.connected_space">pi.connected_space</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/connected.html#pi.totally_disconnected_space">pi.totally_disconnected_space</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/separation.html#pi.t0_space">pi.t0_space</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/separation.html#pi.t1_space">pi.t1_space</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/separation.html#Pi.t2_space">Pi.t2_space</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/separation.html#pi.regular_space">pi.regular_space</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/separation.html#pi.t3_space">pi.t3_space</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/order/basic.html#pi.order_closed_topology">pi.order_closed_topology</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/uniform_space/pi.html#Pi.uniform_space">Pi.uniform_space</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/uniform_space/pi.html#Pi.complete">Pi.complete</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/uniform_space/pi.html#Pi.separated">Pi.separated</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/add_torsor.html#pi.add_torsor">pi.add_torsor</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/algebra/const_mul_action.html#pi.has_continuous_const_smul">pi.has_continuous_const_smul</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/algebra/const_mul_action.html#pi.has_continuous_const_vadd">pi.has_continuous_const_vadd</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/algebra/mul_action.html#pi.has_continuous_smul">pi.has_continuous_smul</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/algebra/mul_action.html#pi.has_continuous_vadd">pi.has_continuous_vadd</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/algebra/monoid.html#pi.has_continuous_mul">pi.has_continuous_mul</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/algebra/monoid.html#pi.has_continuous_add">pi.has_continuous_add</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/algebra/group/basic.html#pi.has_continuous_inv">pi.has_continuous_inv</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/algebra/group/basic.html#pi.has_continuous_neg">pi.has_continuous_neg</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/algebra/group/basic.html#pi.topological_group">pi.topological_group</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/algebra/group/basic.html#pi.topological_add_group">pi.topological_add_group</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/algebra/star.html#pi.has_continuous_star">pi.has_continuous_star</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/algebra/ring/basic.html#pi.topological_semiring">pi.topological_semiring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/algebra/ring/basic.html#pi.topological_ring">pi.topological_ring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/algebra/order/monotone_convergence.html#pi.Sup_convergence_class">pi.Sup_convergence_class</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/algebra/order/monotone_convergence.html#pi.Inf_convergence_class">pi.Inf_convergence_class</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/algebra/order/compact.html#pi.compact_Icc_space">pi.compact_Icc_space</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/order/pi.html#pi.ordered_comm_monoid">pi.ordered_comm_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/order/pi.html#pi.ordered_add_comm_monoid">pi.ordered_add_comm_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/order/pi.html#pi.has_exists_mul_of_le">pi.has_exists_mul_of_le</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/order/pi.html#pi.has_exists_add_of_le">pi.has_exists_add_of_le</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/order/pi.html#pi.canonically_ordered_monoid">pi.canonically_ordered_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/order/pi.html#pi.canonically_ordered_add_monoid">pi.canonically_ordered_add_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/order/pi.html#pi.ordered_cancel_comm_monoid">pi.ordered_cancel_comm_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/order/pi.html#pi.ordered_cancel_add_comm_monoid">pi.ordered_cancel_add_comm_monoid</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/order/pi.html#pi.ordered_comm_group">pi.ordered_comm_group</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/order/pi.html#pi.ordered_add_comm_group">pi.ordered_add_comm_group</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/order/pi.html#pi.ordered_semiring">pi.ordered_semiring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/order/pi.html#pi.ordered_comm_semiring">pi.ordered_comm_semiring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/order/pi.html#pi.ordered_ring">pi.ordered_ring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/order/pi.html#pi.ordered_comm_ring">pi.ordered_comm_ring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/order/smul.html#pi.ordered_smul">pi.ordered_smul</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/metric_space/emetric_space.html#pseudo_emetric_space_pi">pseudo_emetric_space_pi</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/metric_space/emetric_space.html#emetric_space_pi">emetric_space_pi</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/bornology/constructions.html#pi.bornology">pi.bornology</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/bornology/constructions.html#pi.bounded_space">pi.bounded_space</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/metric_space/basic.html#pseudo_metric_space_pi">pseudo_metric_space_pi</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/metric_space/basic.html#pi_proper_space">pi_proper_space</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/metric_space/basic.html#metric_space_pi">metric_space_pi</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/metric_space/isometric_smul.html#pi.has_isometric_smul">pi.has_isometric_smul</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/metric_space/isometric_smul.html#pi.has_isometric_vadd">pi.has_isometric_vadd</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/metric_space/isometric_smul.html#pi.has_isometric_smul'">pi.has_isometric_smul'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/metric_space/isometric_smul.html#pi.has_isometric_vadd'">pi.has_isometric_vadd'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/metric_space/isometric_smul.html#pi.has_isometric_smul''">pi.has_isometric_smul''</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/metric_space/isometric_smul.html#pi.has_isometric_vadd''">pi.has_isometric_vadd''</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/analysis/normed/group/basic.html#pi.seminormed_group">pi.seminormed_group</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/analysis/normed/group/basic.html#pi.seminormed_add_group">pi.seminormed_add_group</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/analysis/normed/group/basic.html#pi.seminormed_comm_group">pi.seminormed_comm_group</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/analysis/normed/group/basic.html#pi.seminormed_add_comm_group">pi.seminormed_add_comm_group</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/analysis/normed/group/basic.html#pi.normed_group">pi.normed_group</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/analysis/normed/group/basic.html#pi.normed_add_group">pi.normed_add_group</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/analysis/normed/group/basic.html#pi.normed_comm_group">pi.normed_comm_group</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/analysis/normed/group/basic.html#pi.normed_add_comm_group">pi.normed_add_comm_group</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/analysis/normed/field/basic.html#pi.norm_one_class">pi.norm_one_class</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/analysis/normed/field/basic.html#pi.non_unital_semi_normed_ring">pi.non_unital_semi_normed_ring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/analysis/normed/field/basic.html#pi.semi_normed_ring">pi.semi_normed_ring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/analysis/normed/field/basic.html#pi.non_unital_normed_ring">pi.non_unital_normed_ring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/analysis/normed/field/basic.html#pi.normed_ring">pi.normed_ring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/analysis/normed_space/basic.html#pi.normed_space">pi.normed_space</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/analysis/normed_space/basic.html#pi.normed_algebra">pi.normed_algebra</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/analysis/normed_space/star/basic.html#pi.star_ring'">pi.star_ring'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/analysis/normed_space/star/basic.html#pi.cstar_ring">pi.cstar_ring</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/path_connected.html#path.has_uncurry_path">path.has_uncurry_path</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/algebra/module/multilinear.html#continuous_multilinear_map.continuous_map_class">continuous_multilinear_map.continuous_map_class</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/category_theory/pi/basic.html#category_theory.pi">category_theory.pi</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/category_theory/pi/basic.html#category_theory.pi'">category_theory.pi'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/category_theory/groupoid.html#category_theory.groupoid_pi">category_theory.groupoid_pi</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/tactic/has_variable_names.html#pi.has_variable_names">pi.has_variable_names</a></li>
</ul>
</details>
<details class="instances-for">
<summary>Instances for <code><span class="name">∀ a : α, β a</span></code></summary>
<ul>
<li><a href="https://pygae.github.io/lean-ga-docs/init/logic.html#forall_prop_decidable">forall_prop_decidable</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/data/list/instances.html#list.decidable_ball">list.decidable_ball</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/option/defs.html#option.decidable_forall_mem">option.decidable_forall_mem</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/bool/basic.html#bool.decidable_forall_bool">bool.decidable_forall_bool</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/tactic/lift.html#pi.can_lift">pi.can_lift</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/nat/basic.html#nat.decidable_ball_lt">nat.decidable_ball_lt</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/nat/basic.html#nat.decidable_forall_fin">nat.decidable_forall_fin</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/nat/basic.html#nat.decidable_ball_le">nat.decidable_ball_le</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/set/image.html#set.can_lift">set.can_lift</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/nat/order/basic.html#nat.decidable_lo_hi">nat.decidable_lo_hi</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/nat/order/basic.html#nat.decidable_lo_hi_le">nat.decidable_lo_hi_le</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/set/list.html#list.can_lift">list.can_lift</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/multiset/basic.html#multiset.can_lift">multiset.can_lift</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/multiset/basic.html#multiset.decidable_dforall_multiset">multiset.decidable_dforall_multiset</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/finset/basic.html#finset.decidable_dforall_finset">finset.decidable_dforall_finset</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/finset/image.html#finset.can_lift">finset.can_lift</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/fintype/basic.html#fintype.decidable_forall_fintype">fintype.decidable_forall_fintype</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/fintype/basic.html#fintype.decidable_surjective_fintype">fintype.decidable_surjective_fintype</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/finset/powerset.html#finset.decidable_forall_of_decidable_subsets">finset.decidable_forall_of_decidable_subsets</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/finset/powerset.html#finset.decidable_forall_of_decidable_ssubsets">finset.decidable_forall_of_decidable_ssubsets</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/topology/instances/nnreal.html#nnreal.continuous_map.can_lift">nnreal.continuous_map.can_lift</a></li>
</ul>
</details>
<details class="instances-for">
<summary>Instances for <code><span class="name">α → β</span></code></summary>
<ul>
<li><a href="https://pygae.github.io/lean-ga-docs/init/coe.html#lift_fn">lift_fn</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/coe.html#lift_fn_range">lift_fn_range</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/coe.html#lift_fn_dom">lift_fn_dom</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/meta/expr.html#expr.has_coe_to_fun">expr.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/meta/interaction_monad.html#interaction_monad.monad">interaction_monad.monad</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/meta/interaction_monad.html#interaction_monad.monad_fail">interaction_monad.monad_fail</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/meta/tactic.html#tactic.alternative">tactic.alternative</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/meta/tactic.html#interactive.executor_tactic">interactive.executor_tactic</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/meta/tactic.html#tactic.opt_to_tac">tactic.opt_to_tac</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/meta/tactic.html#tactic.ex_to_tac">tactic.ex_to_tac</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/meta/tactic.html#tactic.andthen_seq">tactic.andthen_seq</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/meta/tactic.html#tactic.andthen_seq_focus">tactic.andthen_seq_focus</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/meta/lean/parser.html#lean.parser.alternative">lean.parser.alternative</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/meta/lean/parser.html#lean.parser.has_coe">lean.parser.has_coe</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/control/state.html#state_t.monad_run">state_t.monad_run</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/control/reader.html#reader_t.monad_run">reader_t.monad_run</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/meta/smt/smt_tactic.html#smt_tactic.has_monad_lift">smt_tactic.has_monad_lift</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/meta/smt/smt_tactic.html#smt_tactic.has_coe">smt_tactic.has_coe</a></li>
<li>widget.component.has_coe_to_fun</li>
<li><a href="https://pygae.github.io/lean-ga-docs/init/meta/widget/tactic_component.html#widget.tc.has_coe_to_fun">widget.tc.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/meta/expr.html#thunk.has_reflect">thunk.has_reflect</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/tactic/core.html#tactic.tactic.has_to_tactic_format">tactic.tactic.has_to_tactic_format</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/function/basic.html#function.has_uncurry_base">function.has_uncurry_base</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/function/basic.html#function.has_uncurry_induction">function.has_uncurry_induction</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/tactic/lift.html#pi_subtype.can_lift'">pi_subtype.can_lift'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/nontrivial.html#function.nontrivial">function.nontrivial</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/hom/group.html#one_hom.has_coe_to_fun">one_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/hom/group.html#zero_hom.has_coe_to_fun">zero_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/hom/group.html#mul_hom.has_coe_to_fun">mul_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/hom/group.html#add_hom.has_coe_to_fun">add_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/hom/group.html#monoid_hom.has_coe_to_fun">monoid_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/hom/group.html#add_monoid_hom.has_coe_to_fun">add_monoid_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/hom/group.html#monoid_with_zero_hom.has_coe_to_fun">monoid_with_zero_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/equiv/defs.html#equiv.has_coe_to_fun">equiv.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/equiv/basic.html#equiv.function.bijective.can_lift">equiv.function.bijective.can_lift</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/hom/equiv/basic.html#mul_equiv.has_coe_to_fun">mul_equiv.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/hom/equiv/basic.html#add_equiv.has_coe_to_fun">add_equiv.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/boolean_algebra.html#pi.generalized_boolean_algebra">pi.generalized_boolean_algebra</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/set/basic.html#set.pi_set_coe.can_lift'">set.pi_set_coe.can_lift'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/hom/ring.html#non_unital_ring_hom.has_coe_to_fun">non_unital_ring_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/hom/ring.html#ring_hom.has_coe_to_fun">ring_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/embedding/basic.html#function.embedding.has_coe_to_fun">function.embedding.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/embedding/basic.html#function.injective.can_lift">function.injective.can_lift</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/rel_iso/basic.html#rel_hom.has_coe_to_fun">rel_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/rel_iso/basic.html#rel_embedding.has_coe_to_fun">rel_embedding.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/rel_iso/basic.html#rel_iso.has_coe_to_fun">rel_iso.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/hom/basic.html#order_hom.has_coe_to_fun">order_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/hom/basic.html#order_hom.monotone.can_lift">order_hom.monotone.can_lift</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/tactic/abel.html#tactic.abel.normal_expr.has_coe_to_fun">tactic.abel.normal_expr.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/ring/equiv.html#ring_equiv.has_coe_to_fun">ring_equiv.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/hom/group_action.html#mul_action_hom.has_coe_to_fun">mul_action_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/hom/group_action.html#distrib_mul_action_hom.has_coe_to_fun">distrib_mul_action_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/hom/group_action.html#mul_semiring_action_hom.has_coe_to_fun">mul_semiring_action_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#function.has_smul">function.has_smul</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#function.has_vadd">function.has_vadd</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#function.smul_comm_class">function.smul_comm_class</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/group_action/pi.html#function.vadd_comm_class">function.vadd_comm_class</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/module/pi.html#function.module">function.module</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/module/pi.html#function.no_zero_smul_divisors">function.no_zero_smul_divisors</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/module/linear_map.html#linear_map.has_coe_to_fun">linear_map.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/module/equiv.html#linear_equiv.has_coe_to_fun">linear_equiv.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/finset/basic.html#finset.pi_finset_coe.can_lift'">finset.pi_finset_coe.can_lift'</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/hom/bounded.html#top_hom.has_coe_to_fun">top_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/hom/bounded.html#bot_hom.has_coe_to_fun">bot_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/hom/bounded.html#bounded_order_hom.has_coe_to_fun">bounded_order_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/hom/lattice.html#sup_hom.has_coe_to_fun">sup_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/hom/lattice.html#inf_hom.has_coe_to_fun">inf_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/hom/lattice.html#sup_bot_hom.has_coe_to_fun">sup_bot_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/hom/lattice.html#inf_top_hom.has_coe_to_fun">inf_top_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/hom/lattice.html#lattice_hom.has_coe_to_fun">lattice_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/hom/lattice.html#bounded_lattice_hom.has_coe_to_fun">bounded_lattice_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/fin/vec_notation.html#pi_fin.has_repr">pi_fin.has_repr</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/fin/vec_notation.html#pi_fin.reflect">pi_fin.reflect</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/fintype/prod.html#function.infinite_of_left">function.infinite_of_left</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/fintype/prod.html#function.infinite_of_right">function.infinite_of_right</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/finsupp/defs.html#finsupp.has_coe_to_fun">finsupp.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/data/finsupp/defs.html#finsupp.can_lift">finsupp.can_lift</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/order/absolute_value.html#absolute_value.has_coe_to_fun">absolute_value.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/algebra/hom.html#alg_hom.has_coe_to_fun">alg_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/algebra/equiv.html#alg_equiv.has_coe_to_fun">alg_equiv.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/hom/non_unital_alg.html#non_unital_alg_hom.has_coe_to_fun">non_unital_alg_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/congruence.html#con.has_coe_to_fun">con.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/group_theory/congruence.html#add_con.has_coe_to_fun">add_con.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/omega_complete_partial_order.html#omega_complete_partial_order.chain.has_coe_to_fun">omega_complete_partial_order.chain.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/omega_complete_partial_order.html#omega_complete_partial_order.continuous_hom.has_coe_to_fun">omega_complete_partial_order.continuous_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/hom/complete_lattice.html#Sup_hom.has_coe_to_fun">Sup_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/hom/complete_lattice.html#Inf_hom.has_coe_to_fun">Inf_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/hom/complete_lattice.html#frame_hom.has_coe_to_fun">frame_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/order/hom/complete_lattice.html#complete_lattice_hom.has_coe_to_fun">complete_lattice_hom.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/tactic/ring.html#tactic.ring.horner_expr.has_coe_to_fun">tactic.ring.horner_expr.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/equiv/list.html#encodable.fin_arrow">encodable.fin_arrow</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/logic/equiv/list.html#encodable.fintype_arrow_of_encodable">encodable.fintype_arrow_of_encodable</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/linear_algebra/linear_pmap.html#linear_pmap.has_coe_to_fun">linear_pmap.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/for_mathlib/algebra/filtration.html#algebra.filtration.has_coe_to_fun">algebra.filtration.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/monoid_algebra/basic.html#monoid_algebra.has_coe_to_fun">monoid_algebra.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/monoid_algebra/basic.html#add_monoid_algebra.has_coe_to_fun">add_monoid_algebra.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/ring_theory/congruence.html#ring_con.has_coe_to_fun">ring_con.has_coe_to_fun</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/algebra/algebra/pi.html#function.algebra">function.algebra</a></li>
<li><a href="https://pygae.github.io/lean-ga-docs/linear_algebra/free_module/basic.html#module.free.function">module.free.function</a></li>