Mizar articles

• abcmiz_0
• abcmiz_1
• abcmiz_a
• abian
• absred_0
• absvalue
• aescip_1
• aff_1
• aff_2
• aff_3
• aff_4
• afinsq_1
• afinsq_2
• afproj
• afvect0
• afvect01
• aimloop
• alg_1
• alggeo_1
• algnum_1
• algseq_1
• algspec1
• algstr_0
• algstr_1
• algstr_2
• algstr_3
• algstr_4
• ali2
• altcat_1
• altcat_2
• altcat_3
• altcat_4
• altcat_5
• altcat_6
• ami_2
• ami_3
• ami_4
• ami_5
• ami_6
• ami_wstd
• amistd_1
• amistd_2
• amistd_3
• amistd_4
• amistd_5
• analmetr
• analoaf
• analort
• anproj10
• anproj11
• anproj_1
• anproj_2
• anproj_8
• anproj_9
• aofa_000
• aofa_a00
• aofa_a01
• aofa_i00
• aofa_l00
• arithm
• armstrng
• arrow
• arytm_0
• arytm_1
• arytm_2
• arytm_3
• ascoli
• ascoli2
• asympt_0
• asympt_1
• asympt_2
• asympt_3
• autalg_1
• autgroup
• axioms
• bagord_2
• bagorder
• ballot_1
• basel_1
• basel_2
• bcialg_1
• bcialg_2
• bcialg_3
• bcialg_4
• bcialg_5
• bcialg_6
• bciideal
• bhsp_1
• bhsp_2
• bhsp_3
• bhsp_4
• bhsp_5
• bhsp_6
• bhsp_7
• bilinear
• binari_2
• binari_3
• binari_4
• binari_6
• binarith
• binom
• binop_1
• binop_2
• binpack1
• bintree1
• bintree2
• birkhoff
• bkmodel1
• bkmodel2
• bkmodel3
• bkmodel4
• boole
• boolealg
• boolmark
• bor_cant
• borsuk_1
• borsuk_2
• borsuk_3
• borsuk_4
• borsuk_5
• borsuk_6
• borsuk_7
• brouwer
• brouwer2
• brouwer3
• bspace
• bvfunc11
• bvfunc14
• bvfunc25
• bvfunc_1
• bvfunc_2
• bvfunc_3
• bvfunc_4
• bvfunc_5
• bvfunc_6
• c0sp1
• c0sp2
• c0sp3
• calcul_1
• calcul_2
• cantor_1
• card_1
• card_2
• card_3
• card_4
• card_5
• card_fil
• card_fin
• card_lar
• cardfil2
• cardfil3
• cardfil4
• cardfin2
• cat_1
• cat_2
• cat_3
• cat_4
• cat_5
• cat_6
• cat_7
• cat_8
• catalan1
• catalan2
• catalg_1
• cayldick
• cayley
• cc0sp1
• cc0sp2
• cfcont_1
• cfdiff_1
• cfdiff_2
• cfuncdom
• cfunct_1
• cgames_1
• chain_1
• chord
• circcmb2
• circcmb3
• circcomb
• circled1
• circtrm1
• circuit1
• circuit2
• ckspace1
• classes1
• classes2
• classes3
• classes4
• classes5
• clopban1
• clopban2
• clopban3
• clopban4
• closure1
• closure2
• closure3
• clvect_1
• clvect_2
• clvect_3
• coh_sp
• cohsp_1
• collsp
• combgras
• commacat
• compact1
• compl_sp
• complex1
• complex2
• complex3
• complfld
• complsp1
• complsp2
• compos_0
• compos_1
• compos_2
• comptrig
• compts_1
• comput_1
• comseq_1
• comseq_2
• comseq_3
• conaffm
• conlat_1
• conlat_2
• conmetr
• conmetr1
• connsp_1
• connsp_2
• connsp_3
• convex1
• convex2
• convex3
• convex4
• convfun1
• counters
• cousin
• cousin2
• cqc_lang
• cqc_sim1
• cqc_the1
• cqc_the2
• cqc_the3
• csspace
• csspace2
• csspace3
• csspace4
• curve
• dblseq_1
• dblseq_2
• dblseq_3
• decomp_1
• descip_1
• dickson
• diff_1
• diff_2
• diff_3
• diff_4
• dilworth
• diophan1
• diophan2
• diraf
• dirort
• dist_1
• dist_2
• domain_1
• dtconstr
• dualsp01
• dualsp02
• dualsp03
• dualsp04
• dualsp05
• dualsp06
• dynkin
• e_siec
• e_trans1
• e_trans2
• ec_pf_1
• ec_pf_2
• ec_pf_3
• endalg
• ens_1
• entropy1
• enumset1
• eqrel_1
• equation
• euclid
• euclid10
• euclid11
• euclid12
• euclid13
• euclid_2
• euclid_3
• euclid_4
• euclid_5
• euclid_6
• euclid_7
• euclid_8
• euclid_9
• euclidlp
• euclmetr
• euler_1
• euler_2
• eulrpart
• exchsort
• extens_1
• extpro_1
• extreal1
• facirc_1
• facirc_2
• fcont_1
• fcont_2
• fcont_3
• fdiff_1
• fdiff_10
• fdiff_11
• fdiff_12
• fdiff_2
• fdiff_3
• fdiff_4
• fdiff_5
• fdiff_6
• fdiff_7
• fdiff_8
• fdiff_9
• ff_siec
• fib_fusc
• fib_num
• fib_num2
• fib_num3
• fib_num4
• field_1
• field_10
• field_11
• field_12
• field_13
• field_14
• field_15
• field_16
• field_2
• field_3
• field_4
• field_5
• field_6
• field_7
• field_8
• field_9
• filerec1
• filter_0
• filter_1
• filter_2
• fin_topo
• finance1
• finance2
• finance3
• finance4
• finance5
• finance6
• finseq_1
• finseq_2
• finseq_3
• finseq_4
• finseq_5
• finseq_6
• finseq_7
• finseq_8
• finseq_9
• finseqop
• finset_1
• finsop_1
• finsub_1
• fintopo2
• fintopo3
• fintopo4
• fintopo5
• fintopo6
• fintopo7
• fintopo8
• flang_1
• flang_2
• flang_3
• flexary1
• fomodel0
• fomodel1
• fomodel2
• fomodel3
• fomodel4
• fraenkel
• frechet
• frechet2
• freealg
• friends1
• fscirc_1
• fscirc_2
• fsm_1
• fsm_2
• fsm_3
• ftacell1
• funcop_1
• funcsdom
• funct_1
• funct_2
• funct_3
• funct_4
• funct_5
• funct_6
• funct_7
• funct_8
• funct_9
• functor0
• functor1
• functor2
• functor3
• fuzimpl1
• fuzimpl2
• fuzimpl3
• fuzimpl4
• fuznorm1
• fuznum_1
• fuzzy_1
• fuzzy_2
• fuzzy_4
• fuzzy_5
• fuzzy_6
• fuzzy_7
• fuzzy_8
• fvaluat1
• fvsum_1
• gate_1
• gate_2
• gate_3
• gate_4
• gate_5
• gaussint
• gcd_1
• genealg1
• geomtrap
• gfacirc1
• gfacirc2
• glcolo00
• glenum00
• glib_000
• glib_001
• glib_002
• glib_003
• glib_004
• glib_005
• glib_006
• glib_007
• glib_008
• glib_009
• glib_010
• glib_011
• glib_012
• glib_013
• glib_014
• glib_015
• glib_016
• glibpre0
• glibpre1
• glpacy00
• glunir00
• goboard1
• goboard2
• goboard3
• goboard4
• goboard5
• goboard6
• goboard7
• goboard8
• goboard9
• gobrd10
• gobrd11
• gobrd12
• gobrd13
• gobrd14
• goedcpuc
• goedelcp
• gr_cy_1
• gr_cy_2
• gr_cy_3
• gr_free0
• graph_1
• graph_2
• graph_3
• graph_3a
• graph_4
• graph_5
• graphsp
• grcat_1
• grfunc_1
• grnilp_1
• groeb_1
• groeb_2
• groeb_3
• group_1
• group_10
• group_11
• group_12
• group_14
• group_17
• group_18
• group_19
• group_1a
• group_2
• group_20
• group_21
• group_22
• group_23
• group_24
• group_3
• group_4
• group_5
• group_6
• group_7
• group_8
• group_9
• groupp_1
• grsolv_1
• grzlog_1
• gtarski1
• gtarski2
• gtarski3
• gtarski4
• gtarski5
• hahnban
• hahnban1
• hallmar1
• hausdorf
• heine
• helly
• henmodel
• hermitan
• hessenbe
• heyting1
• heyting2
• heyting3
• hfdiff_1
• hidden
• hilb10_1
• hilb10_2
• hilb10_3
• hilb10_4
• hilb10_5
• hilb10_6
• hilb10_7
• hilb10_8
• hilbasis
• hilbert1
• hilbert2
• hilbert3
• hilbert4
• holder_1
• homothet
• huffman1
• hurwitz
• hurwitz2
• idea_1
• ideal_1
• ideal_2
• incproj
• incsp_1
• index_1
• instalg1
• int_1
• int_2
• int_3
• int_4
• int_5
• int_6
• int_7
• int_8
• integr10
• integr11
• integr12
• integr13
• integr14
• integr15
• integr16
• integr18
• integr19
• integr1c
• integr20
• integr21
• integr22
• integr23
• integr24
• integr25
• integr26
• integra1
• integra2
• integra3
• integra4
• integra5
• integra6
• integra7
• integra8
• integra9
• interva1
• intpro_1
• intpro_2
• irrat_1
• isocat_1
• isocat_2
• isomichi
• jct_misc
• jgraph_1
• jgraph_2
• jgraph_3
• jgraph_4
• jgraph_5
• jgraph_6
• jgraph_7
• jgraph_8
• jordan
• jordan1
• jordan10
• jordan11
• jordan12
• jordan13
• jordan14
• jordan15
• jordan16
• jordan17
• jordan18
• jordan19
• jordan1a
• jordan1b
• jordan1c
• jordan1d
• jordan1e
• jordan1f
• jordan1g
• jordan1h
• jordan1i
• jordan1j
• jordan1k
• jordan20
• jordan21
• jordan22
• jordan23
• jordan24
• jordan2b
• jordan2c
• jordan3
• jordan4
• jordan5a
• jordan5b
• jordan5c
• jordan5d
• jordan6
• jordan7
• jordan8
• jordan9
• jordan_a
• knaster
• kolmog01
• kurato_0
• kurato_1
• kurato_2
• l_hospit
• lagra4sq
• lang1
• laplace
• latquasi
• latstone
• latsubgr
• latsum_1
• lattad_1
• lattba_1
• lattice2
• lattice3
• lattice4
• lattice5
• lattice6
• lattice7
• lattice8
• latticea
• lattices
• latwal_1
• latwal_2
• leibniz1
• lexbfs
• lfuzzy_0
• lfuzzy_1
• limfunc1
• limfunc2
• limfunc3
• limfunc4
• liouvil1
• liouvil2
• lmod_6
• lmod_7
• lmod_xx1
• lopban10
• lopban11
• lopban12
• lopban13
• lopban14
• lopban15
• lopban_1
• lopban_2
• lopban_3
• lopban_4
• lopban_5
• lopban_6
• lopban_7
• lopban_8
• lopban_9
• lopclset
• lp_space
• lpspacc1
• lpspace1
• lpspace2
• ltlaxio1
• ltlaxio2
• ltlaxio3
• ltlaxio4
• ltlaxio5
• lukasi_1
• margrel1
• mathmorp
• matrix10
• matrix11
• matrix12
• matrix13
• matrix14
• matrix15
• matrix16
• matrix17
• matrix_0
• matrix_1
• matrix_3
• matrix_4
• matrix_5
• matrix_6
• matrix_7
• matrix_8
• matrix_9
• matrixc1
• matrixj1
• matrixj2
• matrixr1
• matrixr2
• matrlin
• matrlin2
• matroid0
• matrprob
• matrtop1
• matrtop2
• matrtop3
• mazurulm
• mboolean
• mcart_1
• measur10
• measur11
• measur12
• measur13
• measur14
• measure1
• measure2
• measure3
• measure4
• measure5
• measure6
• measure7
• measure8
• measure9
• member_1
• membered
• memstr_0
• menelaus
• mesfun10
• mesfun11
• mesfun12
• mesfun13
• mesfun14
• mesfun15
• mesfun16
• mesfun17
• mesfun6c
• mesfun7c
• mesfun9c
• mesfunc1
• mesfunc2
• mesfunc3
• mesfunc4
• mesfunc5
• mesfunc6
• mesfunc7
• mesfunc8
• mesfunc9
• metric_1
• metric_2
• metric_3
• metric_6
• metrizts
• mfold_0
• mfold_1
• mfold_2
• midsp_1
• midsp_2
• midsp_3
• mmlquer2
• mmlquery
• mod_2
• mod_3
• mod_4
• modal_1
• modcat_1
• modelc_1
• modelc_2
• modelc_3
• moebius1
• moebius2
• moebius3
• monoid_0
• monoid_1
• morph_01
• msafree
• msafree1
• msafree2
• msafree3
• msafree4
• msafree5
• msalimit
• msaterm
• msinst_1
• msscyc_1
• msscyc_2
• mssubfam
• mssublat
• msualg_1
• msualg_2
• msualg_3
• msualg_4
• msualg_5
• msualg_6
• msualg_7
• msualg_8
• msualg_9
• msuhom_1
• multop_1
• music_s1
• mycielsk
• nagata_1
• nagata_2
• nat_1
• nat_2
• nat_3
• nat_4
• nat_5
• nat_6
• nat_d
• nat_lat
• nattra_1
• nbvectsp
• ncfcont1
• ncfcont2
• ndiff10
• ndiff11
• ndiff12
• ndiff13
• ndiff_1
• ndiff_2
• ndiff_3
• ndiff_4
• ndiff_5
• ndiff_6
• ndiff_7
• ndiff_8
• ndiff_9
• neckla_2
• neckla_3
• necklace
• nelson_1
• net_1
• neurons1
• newton
• newton01
• newton02
• newton03
• newton04
• newton05
• newton06
• newton07
• nfcont_1
• nfcont_2
• nfcont_3
• nfcont_4
• niven
• nomin_1
• nomin_2
• nomin_3
• nomin_4
• nomin_5
• nomin_6
• nomin_7
• nomin_8
• nomin_9
• normform
• normsp_0
• normsp_1
• normsp_2
• normsp_3
• normsp_4
• ntalgo_1
• ntalgo_2
• number01
• number02
• number03
• number04
• number05
• number06
• number07
• number08
• number09
• number10
• number11
• number12
• number13
• number14
• number15
• number16
• numbers
• numeral1
• numeral2
• numerals
• numpoly1
• o_ring_1
• openlatt
• oposet_1
• oppcat_1
• ordeq_01
• ordeq_02
• orders_1
• orders_2
• orders_3
• orders_4
• orders_5
• ordinal1
• ordinal2
• ordinal3
• ordinal4
• ordinal5
• ordinal6
• ordinal7
• ortsp_1
• osafree
• osalg_1
• osalg_2
• osalg_3
• osalg_4
• papdesaf
• pappus
• pardepap
• parsp_1
• parsp_2
• partfun1
• partfun2
• partfun3
• partfun4
• partit1
• partit_2
• partpr_1
• partpr_2
• pascal
• pasch
• pboole
• pcomps_1
• pcomps_2
• pcs_0
• pdiff_1
• pdiff_2
• pdiff_3
• pdiff_4
• pdiff_5
• pdiff_6
• pdiff_7
• pdiff_8
• pdiff_9
• pdiffeq1
• pdlax
• pells_eq
• pencil_1
• pencil_2
• pencil_3
• pencil_4
• pepin
• peterson
• petri
• petri_2
• petri_3
• petri_df
• pl_axiom
• pnproc_1
• polnot_1
• polnot_2
• polyalg1
• polyalgx
• polydiff
• polyeq_1
• polyeq_2
• polyeq_3
• polyeq_4
• polyeq_5
• polyform
• polynom1
• polynom2
• polynom3
• polynom4
• polynom5
• polynom6
• polynom7
• polynom8
• polynom9
• polyred
• polyvie1
• poset_1
• poset_2
• power
• pralg_1
• pralg_2
• pralg_3
• pre_circ
• pre_ff
• pre_poly
• pre_topc
• prefer_1
• prelamb
• prepower
• prgcor_1
• prgcor_2
• primreci
• prob_1
• prob_2
• prob_3
• prob_4
• procal_1
• projdes1
• projpl_1
• projred1
• projred2
• proofs_1
• prsubset
• prvect_1
• prvect_2
• prvect_3
• prvect_4
• pscomp_1
• pua2mss1
• pythtrip
• pzfmisc1
• qc_lang1
• qc_lang2
• qc_lang3
• qc_lang4
• qc_trans
• qmax_1
• quantal1
• quatern2
• quatern3
• quaterni
• quin_1
• quofield
• radix_1
• radix_2
• radix_3
• radix_4
• radix_5
• radix_6
• ramsey_1
• random_1
• random_2
• random_3
• ranknull
• rat_1
• ratfunc1
• rcomp_1
• rcomp_3
• real
• real_1
• real_3
• real_lat
• real_ns1
• real_ns2
• real_ns3
• realalg1
• realalg2
• realalg3
• realset1
• realset2
• realset3
• rearran1
• recdef_1
• recdef_2
• relat_1
• relat_2
• reloc
• relset_1
• relset_2
• relset_3
• revrot_1
• rewrite1
• rewrite2
• rewrite3
• rfinseq
• rfinseq2
• rfunct_1
• rfunct_2
• rfunct_3
• rfunct_4
• rinfsup1
• rinfsup2
• ring_1
• ring_2
• ring_3
• ring_4
• ring_5
• ring_emb
• ringcat1
• ringder1
• ringfrac
• rlaffin1
• rlaffin2
• rlaffin3
• rlsub_1
• rlsub_2
• rltopsp1
• rlvect_1
• rlvect_2
• rlvect_3
• rlvect_4
• rlvect_5
• rlvect_x
• rmod_2
• rmod_3
• rmod_4
• robbins1
• robbins2
• robbins3
• robbins4
• robbins5
• rolle
• roughif1
• roughif2
• roughs_1
• roughs_2
• roughs_3
• roughs_4
• roughs_5
• rpr_1
• rsspace
• rsspace2
• rsspace3
• rsspace4
• rusub_1
• rusub_2
• rusub_3
• rusub_4
• rusub_5
• rusub_6
• rusub_7
• rvsum_1
• rvsum_2
• rvsum_3
• rvsum_4
• scheme1
• schems_1
• scm_1
• scm_comp
• scm_halt
• scm_inst
• scmbsort
• scmfsa10
• scmfsa6a
• scmfsa6b
• scmfsa6c
• scmfsa7b
• scmfsa8a
• scmfsa8b
• scmfsa8c
• scmfsa9a
• scmfsa_1
• scmfsa_2
• scmfsa_3
• scmfsa_4
• scmfsa_5
• scmfsa_7
• scmfsa_9
• scmfsa_i
• scmfsa_m
• scmfsa_x
• scmisort
• scmp_gcd
• scmpds_1
• scmpds_2
• scmpds_3
• scmpds_4
• scmpds_5
• scmpds_6
• scmpds_7
• scmpds_8
• scmpds_9
• scmpds_i
• scmring1
• scmring2
• scmring3
• scmring4
• scmringi
• scmyciel
• scpinvar
• scpisort
• scpqsort
• semi_af1
• seq_1
• seq_2
• seq_4
• seqfunc
• seqfunc2
• seqm_3
• series_1
• series_2
• series_3
• series_4
• series_5
• setfam_1
• setlim_1
• setlim_2
• setwiseo
• setwop_2
• sf_mastr
• sfmastr1
• sfmastr2
• sfmastr3
• sgraph1
• sheffer1
• sheffer2
• simplex0
• simplex1
• simplex2
• sin_cos
• sin_cos2
• sin_cos3
• sin_cos4
• sin_cos5
• sin_cos6
• sin_cos7
• sin_cos8
• sin_cos9
• sincos10
• sppol_1
• sppol_2
• sprect_1
• sprect_2
• sprect_3
• sprect_4
• sprect_5
• square_1
• srings_1
• srings_2
• srings_3
• srings_4
• srings_5
• stacks_1
• stirl2_1
• struct_0
• sublemma
• subset
• subset_1
• substlat
• substut1
• substut2
• supinf_1
• supinf_2
• surreal0
• surrealc
• surreali
• surrealn
• surrealo
• surrealr
• surreals
• symsp_1
• sysrel
• t_0topsp
• t_1topsp
• tarski
• tarski_0
• tarski_a
• taxonom1
• taxonom2
• taylor_1
• taylor_2
• tbsp_1
• tdgroup
• tdlat_1
• tdlat_2
• tdlat_3
• termord
• tex_1
• tex_2
• tex_3
• tex_4
• tietze
• tietze_2
• tmap_1
• toler_1
• topalg_1
• topalg_2
• topalg_3
• topalg_4
• topalg_5
• topalg_6
• topalg_7
• topdim_1
• topdim_2
• topgen_1
• topgen_2
• topgen_3
• topgen_4
• topgen_5
• topgen_6
• topgrp_1
• topmetr
• topmetr2
• topmetr3
• topmetr4
• topreal1
• topreal2
• topreal3
• topreal4
• topreal5
• topreal6
• topreal7
• topreal8
• topreal9
• topreala
• toprealb
• toprealc
• toprns_1
• tops_1
• tops_2
• tops_3
• tops_4
• tops_5
• topzari1
• transgeo
• translac
• treal_1
• trees_1
• trees_2
• trees_3
• trees_4
• trees_9
• trees_a
• triang_1
• tsep_1
• tsep_2
• tsp_1
• tsp_2
• turing_1
• twoscomp
• unialg_1
• unialg_2
• unialg_3
• uniform1
• uniform2
• uniform3
• uniroots
• uproots
• urysohn1
• urysohn2
• urysohn3
• valuat_1
• valued_0
• valued_1
• valued_2
• vectmetr
• vectsp10
• vectsp11
• vectsp12
• vectsp13
• vectsp_1
• vectsp_2
• vectsp_4
• vectsp_5
• vectsp_6
• vectsp_7
• vectsp_8
• vectsp_9
• vfunct_1
• vfunct_2
• vsdiff_1
• wallace1
• waybel10
• waybel11
• waybel12
• waybel13
• waybel14
• waybel15
• waybel16
• waybel17
• waybel18
• waybel19
• waybel20
• waybel21
• waybel22
• waybel23
• waybel24
• waybel25
• waybel26
• waybel27
• waybel28
• waybel29
• waybel30
• waybel31
• waybel32
• waybel33
• waybel34
• waybel35
• waybel_0
• waybel_1
• waybel_2
• waybel_3
• waybel_4
• waybel_5
• waybel_6
• waybel_7
• waybel_8
• waybel_9
• weddwitt
• weierstr
• wellfnd1
• wellord1
• wellord2
• wellset1
• wsierp_1
• xboole_0
• xboole_1
• xboolean
• xcmplx_0
• xcmplx_1
• xfamily
• xprimes0
• xprimes1
• xprimes2
• xprimet1
• xreal_0
• xreal_1
• xregular
• xtuple_0
• xxreal_0
• xxreal_1
• xxreal_2
• xxreal_3
• yellow10
• yellow11
• yellow12
• yellow13
• yellow14
• yellow15
• yellow16
• yellow17
• yellow18
• yellow19
• yellow20
• yellow21
• yellow_0
• yellow_1
• yellow_2
• yellow_3
• yellow_4
• yellow_5
• yellow_6
• yellow_7
• yellow_8
• yellow_9
• yoneda_1
• zf_colla
• zf_fund1
• zf_fund2
• zf_lang
• zf_lang1
• zf_model
• zf_refle
• zfmisc_1
• zfmodel1
• zfmodel2
• zfrefle1
• zmatrlin
• zmodlat1
• zmodlat2
• zmodlat3
• zmodul01
• zmodul02
• zmodul03
• zmodul04
• zmodul05
• zmodul06
• zmodul07
• zmodul08