Last active
August 13, 2019 03:38
-
-
Save fpvandoorn/bdc82881ba8e6461460e8028c291162f to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/- All declarations in mathlib that | |
* are a lemma/theorem but construct data | |
* are a definition, but define an element of a proposition | |
All automatically generated definitions and all instances are filtered out. | |
-/ | |
-- topology\uniform_space\uniform_embedding.lean | |
#print uniform_inducing.mk' -- is a def, should be a lemma/theorem | |
-- topology\order.lean | |
#print continuous_iff_continuous_on_univ -- is a def, should be a lemma/theorem | |
-- topology\opens.lean | |
#print topological_space.opens.gc -- is a def, should be a lemma/theorem | |
-- topology\metric_space\isometry.lean | |
#print isometry.isometric_on_range -- is a lemma/theorem, should be a def | |
-- topology\maps.lean | |
#print embedding.mk' -- is a def, should be a lemma/theorem | |
#print dense_range.inhabited -- is a lemma/theorem, should be a def | |
-- topology\constructions.lean | |
#print homeomorph.continuous -- is a def, should be a lemma/theorem | |
#print dense_embedding.prod -- is a def, should be a lemma/theorem | |
#print dense_embedding.subtype -- is a def, should be a lemma/theorem | |
#print dense_inducing.prod -- is a def, should be a lemma/theorem | |
-- topology\algebra\group.lean | |
#print nhds_is_add_hom -- is a def, should be a lemma/theorem | |
#print nhds_is_mul_hom -- is a def, should be a lemma/theorem | |
-- tactic\omega\nat\preterm.lean | |
#print omega.nat.preterm.val_constant -- is a def, should be a lemma/theorem | |
-- tactic\omega\nat\form.lean | |
#print omega.nat.form.holds_constant -- is a def, should be a lemma/theorem | |
-- tactic\omega\coeffs.lean | |
#print omega.coeffs.val_set -- is a def, should be a lemma/theorem | |
#print omega.coeffs.val_except_add_eq -- is a def, should be a lemma/theorem | |
#print omega.coeffs.val_between_set -- is a def, should be a lemma/theorem | |
-- tactic\omega\clause.lean | |
#print omega.clause.holds_append -- is a def, should be a lemma/theorem | |
-- tactic\monotonicity\interactive.lean | |
#print tactic.interactive.apply_rel -- is a lemma/theorem, should be a def | |
-- tactic\interactive.lean | |
#print tactic.interactive.generalize_a_aux -- is a lemma/theorem, should be a def | |
-- tactic\chain.lean | |
#print tactic.tactic_script.base.inj_eq -- is a def, should be a lemma/theorem | |
#print tactic.tactic_script.pack_1_2.inj -- is a def, should be a lemma/theorem | |
#print tactic.tactic_script.primitive.pack_unpack -- is a def, should be a lemma/theorem | |
#print tactic.tactic_script.work.sizeof_spec -- is a def, should be a lemma/theorem | |
#print tactic.tactic_script.unpack_pack_1_2 -- is a def, should be a lemma/theorem | |
#print tactic.tactic_script.work.inj_eq -- is a def, should be a lemma/theorem | |
#print tactic.tactic_script.primitive.pack.list.nil.spec -- is a def, should be a lemma/theorem | |
#print tactic.tactic_script.sizeof_pack_1_2 -- is a def, should be a lemma/theorem | |
#print tactic.tactic_script.base.inj -- is a def, should be a lemma/theorem | |
#print tactic.tactic_script.base.sizeof_spec -- is a def, should be a lemma/theorem | |
#print tactic.tactic_script.primitive.pack.list.cons.spec -- is a def, should be a lemma/theorem | |
#print tactic.tactic_script.primitive.pack.inj -- is a def, should be a lemma/theorem | |
#print tactic.tactic_script.pack_unpack_1_2 -- is a def, should be a lemma/theorem | |
#print tactic.tactic_script.primitive.unpack_pack -- is a def, should be a lemma/theorem | |
#print tactic.tactic_script.primitive.sizeof_pack -- is a def, should be a lemma/theorem | |
#print tactic.tactic_script.work.inj -- is a def, should be a lemma/theorem | |
-- set_theory\zfc.lean | |
#print classical.all_definable -- is a lemma/theorem, should be a def | |
-- set_theory\ordinal.lean | |
#print cardinal.ord_eq_min -- is a def, should be a lemma/theorem | |
#print embedding_to_cardinal -- is a lemma/theorem, should be a def | |
#print ordinal.div_def -- is a def, should be a lemma/theorem | |
-- set_theory\lists.lean | |
#print lists'.subset.nil -- is a def, should be a lemma/theorem | |
#print lists'.subset.cons -- is a def, should be a lemma/theorem | |
#print lists'.subset.rec -- is a def, should be a lemma/theorem | |
#print lists'.subset.cases_on -- is a def, should be a lemma/theorem | |
#print lists.equiv.antisymm -- is a def, should be a lemma/theorem | |
#print lists.equiv.refl -- is a def, should be a lemma/theorem | |
#print lists.equiv.rec -- is a def, should be a lemma/theorem | |
#print lists.equiv.cases_on -- is a def, should be a lemma/theorem | |
-- ring_theory\power_series.lean | |
#print mv_power_series.is_local_ring -- is a def, should be a lemma/theorem | |
-- ring_theory\ideals.lean | |
#print ideal.zero_ne_one_of_proper -- is a def, should be a lemma/theorem | |
-- ring_theory\algebra.lean | |
#print algebra.gc -- is a def, should be a lemma/theorem | |
-- order\order_iso.lean | |
#print order_iso.prod_lex_congr -- is a lemma/theorem, should be a def | |
#print order_iso.sum_lex_congr -- is a lemma/theorem, should be a def | |
#print order_embedding.nat_lt -- is a lemma/theorem, should be a def | |
#print order_embedding.nat_gt -- is a lemma/theorem, should be a def | |
-- order\filter\pointwise.lean | |
#print filter.pointwise_mul_map_is_monoid_hom -- is a def, should be a lemma/theorem | |
#print filter.pointwise_add_map_is_add_monoid_hom -- is a def, should be a lemma/theorem | |
-- order\filter\partial.lean | |
#print filter.mem_pmap -- is a def, should be a lemma/theorem | |
#print filter.mem_rcomap' -- is a def, should be a lemma/theorem | |
-- order\filter\basic.lean | |
#print filter.is_lawful_monad -- is a def, should be a lemma/theorem | |
-- order\complete_lattice.lean | |
#print lattice.has_Inf_to_nonempty -- is a def, should be a lemma/theorem | |
#print lattice.has_Sup_to_nonempty -- is a def, should be a lemma/theorem | |
-- order\basic.lean | |
#print antisymm_of_asymm -- is a def, should be a lemma/theorem | |
#print well_founded.lt_sup -- is a def, should be a lemma/theorem | |
-- number_theory\dioph.lean | |
#print poly.ext -- is a def, should be a lemma/theorem | |
#print poly.isp -- is a def, should be a lemma/theorem | |
#print poly.induction -- is a def, should be a lemma/theorem | |
-- measure_theory\ae_eq_fun.lean | |
#print measure_theory.ae_eq_fun.lift_rel_mk_mk -- is a def, should be a lemma/theorem | |
-- logic\basic.lean | |
#print imp_intro -- is a lemma/theorem, should be a def | |
#print not.elim -- is a lemma/theorem, should be a def | |
#print Exists.imp -- is a def, should be a lemma/theorem | |
#print classical.dec_rel -- is a lemma/theorem, should be a def | |
#print classical.dec_eq -- is a lemma/theorem, should be a def | |
#print classical.dec_pred -- is a lemma/theorem, should be a def | |
#print classical.dec -- is a lemma/theorem, should be a def | |
-- linear_algebra\finsupp_vector_space.lean | |
#print fin_dim_vectorspace_equiv -- is a lemma/theorem, should be a def | |
-- group_theory\sylow.lean | |
#print sylow.fixed_points_mul_left_cosets_equiv_quotient -- is a lemma/theorem, should be a def | |
-- group_theory\free_group.lean | |
#print free_group.to_word.inj -- is a def, should be a lemma/theorem | |
#print free_group.to_word.mk -- is a def, should be a lemma/theorem | |
-- data\seq\computation.lean | |
#print computation.lift_rel_aux.ret_left -- is a def, should be a lemma/theorem | |
#print computation.corec_eq -- is a def, should be a lemma/theorem | |
#print computation.lift_rel_aux.ret_right -- is a def, should be a lemma/theorem | |
-- data\rat\order.lean | |
#print rat.nonneg_antisymm -- is a def, should be a lemma/theorem | |
#print rat.nonneg_add -- is a def, should be a lemma/theorem | |
#print rat.nonneg_total -- is a def, should be a lemma/theorem | |
#print rat.nonneg_mul -- is a def, should be a lemma/theorem | |
-- data\rat\basic.lean | |
#print rat.num_denom_cases_on -- is a lemma/theorem, should be a def | |
#print rat.num_denom_cases_on' -- is a lemma/theorem, should be a def | |
-- data\polynomial.lean | |
#print polynomial.degree_lt_wf -- is a def, should be a lemma/theorem | |
-- data\pfun.lean | |
#print pfun.fix_induction -- is a lemma/theorem, should be a def | |
#print roption.ext -- is a def, should be a lemma/theorem | |
#print pfun.ext -- is a def, should be a lemma/theorem | |
#print pfun.ext' -- is a def, should be a lemma/theorem | |
#print roption.ext' -- is a def, should be a lemma/theorem | |
#print pfun.mem_preimage -- is a def, should be a lemma/theorem | |
-- data\matrix\basic.lean | |
#print matrix.is_add_monoid_hom_mul_right -- is a def, should be a lemma/theorem | |
-- data\list\min_max.lean | |
#print list.minimum_singleton -- is a def, should be a lemma/theorem | |
#print list.minimum_aux_cons -- is a def, should be a lemma/theorem | |
#print list.maximum_cons -- is a def, should be a lemma/theorem | |
#print list.maximum_singleton -- is a def, should be a lemma/theorem | |
#print list.minimum_cons -- is a def, should be a lemma/theorem | |
#print list.maximum_aux_cons -- is a def, should be a lemma/theorem | |
-- data\finsupp.lean | |
#print finsupp.lt_wf -- is a def, should be a lemma/theorem | |
-- data\finset.lean | |
#print finset.strong_induction_on -- is a lemma/theorem, should be a def | |
-- data\fin.lean | |
#print fin.mk_val -- is a def, should be a lemma/theorem | |
-- data\equiv\basic.lean | |
#print equiv.subtype_quotient_equiv_quotient_subtype -- is a lemma/theorem, should be a def | |
-- data\equiv\algebra.lean | |
#print mul_equiv.apply_symm_apply -- is a def, should be a lemma/theorem | |
#print add_equiv.map_zero -- is a def, should be a lemma/theorem | |
#print add_equiv.map_add -- is a def, should be a lemma/theorem | |
#print mul_equiv.symm_apply_apply -- is a def, should be a lemma/theorem | |
#print mul_equiv.map_one -- is a def, should be a lemma/theorem | |
#print add_equiv.apply_symm_apply -- is a def, should be a lemma/theorem | |
#print add_equiv.symm_apply_apply -- is a def, should be a lemma/theorem | |
#print mul_equiv.map_mul -- is a def, should be a lemma/theorem | |
-- computability\turing_machine.lean | |
#print turing.TM2to1.stmt_st_rec -- is a lemma/theorem, should be a def | |
-- category_theory\natural_transformation.lean | |
#print category_theory.nat_trans.naturality -- is a def, should be a lemma/theorem | |
-- category_theory\natural_isomorphism.lean | |
#print category_theory.nat_iso.of_components.inv_app -- is a def, should be a lemma/theorem | |
#print category_theory.nat_iso.of_components.hom_app -- is a def, should be a lemma/theorem | |
#print category_theory.nat_iso.of_components.app -- is a def, should be a lemma/theorem | |
-- category_theory\monoidal\functor.lean | |
#print category_theory.lax_monoidal_functor.left_unitality -- is a def, should be a lemma/theorem | |
#print category_theory.lax_monoidal_functor.right_unitality -- is a def, should be a lemma/theorem | |
#print category_theory.lax_monoidal_functor.associativity -- is a def, should be a lemma/theorem | |
#print category_theory.lax_monoidal_functor.μ_natural -- is a def, should be a lemma/theorem | |
-- category_theory\monoidal\category.lean | |
#print category_theory.monoidal_category.triangle -- is a def, should be a lemma/theorem | |
#print category_theory.monoidal_category.tensor_id -- is a def, should be a lemma/theorem | |
#print category_theory.monoidal_category.right_unitor_naturality -- is a def, should be a lemma/theorem | |
#print category_theory.monoidal_category.left_unitor_naturality -- is a def, should be a lemma/theorem | |
#print category_theory.monoidal_category.pentagon -- is a def, should be a lemma/theorem | |
#print category_theory.monoidal_category.associator_naturality -- is a def, should be a lemma/theorem | |
#print category_theory.monoidal_category.tensor_comp -- is a def, should be a lemma/theorem | |
-- category_theory\monad\basic.lean | |
#print category_theory.monad.assoc -- is a def, should be a lemma/theorem | |
#print category_theory.monad.right_unit -- is a def, should be a lemma/theorem | |
#print category_theory.monad.left_unit -- is a def, should be a lemma/theorem | |
-- category_theory\monad\algebra.lean | |
#print category_theory.monad.algebra.hom.h -- is a def, should be a lemma/theorem | |
#print category_theory.monad.algebra.assoc -- is a def, should be a lemma/theorem | |
#print category_theory.monad.algebra.unit -- is a def, should be a lemma/theorem | |
-- category_theory\limits\shapes\equalizers.lean | |
#print category_theory.limits.fork.condition -- is a def, should be a lemma/theorem | |
#print category_theory.limits.cofork.condition -- is a def, should be a lemma/theorem | |
-- category_theory\limits\limits.lean | |
#print category_theory.limits.is_limit.uniq -- is a def, should be a lemma/theorem | |
#print category_theory.limits.is_colimit.uniq -- is a def, should be a lemma/theorem | |
#print category_theory.limits.is_colimit.fac -- is a def, should be a lemma/theorem | |
#print category_theory.limits.is_limit.fac -- is a def, should be a lemma/theorem | |
-- category_theory\limits\cones.lean | |
#print category_theory.limits.cocone_morphism.w -- is a def, should be a lemma/theorem | |
#print category_theory.limits.cone_morphism.w -- is a def, should be a lemma/theorem | |
-- category_theory\isomorphism.lean | |
#print category_theory.iso.hom_inv_id -- is a def, should be a lemma/theorem | |
#print category_theory.iso.inv_hom_id -- is a def, should be a lemma/theorem | |
-- category_theory\groupoid.lean | |
#print category_theory.groupoid.inv_comp -- is a def, should be a lemma/theorem | |
#print category_theory.groupoid.comp_inv -- is a def, should be a lemma/theorem | |
-- category_theory\functor.lean | |
#print category_theory.functor.map_comp -- is a def, should be a lemma/theorem | |
#print category_theory.functor.map_id -- is a def, should be a lemma/theorem | |
-- category_theory\fully_faithful.lean | |
#print category_theory.faithful.injectivity -- is a def, should be a lemma/theorem | |
#print category_theory.functor.injectivity -- is a def, should be a lemma/theorem | |
#print category_theory.full.witness -- is a def, should be a lemma/theorem | |
-- category_theory\equivalence.lean | |
#print category_theory.is_equivalence.functor_unit_iso_comp -- is a def, should be a lemma/theorem | |
#print category_theory.equivalence.functor_unit_iso_comp -- is a def, should be a lemma/theorem | |
-- category_theory\comma.lean | |
#print category_theory.comma_morphism.w -- is a def, should be a lemma/theorem | |
-- category_theory\category.lean | |
#print category_theory.category.comp_id -- is a def, should be a lemma/theorem | |
#print category_theory.category.id_comp -- is a def, should be a lemma/theorem | |
#print category_theory.category.assoc -- is a def, should be a lemma/theorem | |
-- category_theory\adjunction\basic.lean | |
#print category_theory.adjunction.core_unit_counit.left_triangle -- is a def, should be a lemma/theorem | |
#print category_theory.adjunction.core_unit_counit.right_triangle -- is a def, should be a lemma/theorem | |
#print category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_right -- is a def, should be a lemma/theorem | |
#print category_theory.adjunction.hom_equiv_unit -- is a def, should be a lemma/theorem | |
#print category_theory.adjunction.hom_equiv_counit -- is a def, should be a lemma/theorem | |
#print category_theory.adjunction.core_hom_equiv.hom_equiv_naturality_left_symm -- is a def, should be a lemma/theorem | |
-- category\traversable\equiv.lean | |
#print equiv.is_lawful_functor' -- is a def, should be a lemma/theorem | |
#print equiv.is_lawful_functor -- is a def, should be a lemma/theorem | |
-- algebra\ring.lean | |
#print is_ring_hom.of_semiring -- is a def, should be a lemma/theorem | |
-- algebra\pointwise.lean | |
#print set.singleton.is_monoid_hom -- is a def, should be a lemma/theorem | |
#print set.singleton.is_add_monoid_hom -- is a def, should be a lemma/theorem | |
#print set.singleton.is_mul_hom -- is a def, should be a lemma/theorem | |
#print set.singleton.is_add_hom -- is a def, should be a lemma/theorem | |
#print set.pointwise_mul_image_is_semiring_hom -- is a def, should be a lemma/theorem | |
-- algebra\ordered_field.lean | |
#print div_nonneg -- is a def, should be a lemma/theorem | |
#print div_pos -- is a def, should be a lemma/theorem | |
#print half_lt_self -- is a def, should be a lemma/theorem | |
-- algebra\order_functions.lean | |
#print abs_add -- is a def, should be a lemma/theorem | |
#print sub_abs_le_abs_sub -- is a def, should be a lemma/theorem | |
-- algebra\group\hom.lean | |
#print monoid_hom.ext -- is a def, should be a lemma/theorem | |
#print add_monoid_hom.map_add -- is a def, should be a lemma/theorem | |
#print add_monoid_hom.ext -- is a def, should be a lemma/theorem | |
#print add_monoid_hom.map_zero -- is a def, should be a lemma/theorem | |
-- algebra\group\basic.lean | |
#print sub_sub_cancel -- is a def, should be a lemma/theorem | |
-- algebra\direct_limit.lean | |
#print add_comm_group.direct_limit.directed_system -- is a def, should be a lemma/theorem |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment