Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-07-23 18:59 4a285354

View on Github →

refactor(*): attributes on same line

Estimated changes

modified theorem lattice.inf_neg_eq_bot
modified theorem lattice.neg_bot
modified theorem lattice.neg_eq_neg_iff
modified theorem lattice.neg_inf
modified theorem lattice.neg_inf_eq_bot
modified theorem lattice.neg_neg
modified theorem lattice.neg_sup
modified theorem lattice.neg_sup_eq_top
modified theorem lattice.neg_top
modified theorem lattice.sup_neg_eq_top
modified theorem lattice.Inf_empty
modified theorem lattice.Inf_insert
modified theorem lattice.Inf_le
modified theorem lattice.Inf_le_iff
modified theorem lattice.Inf_singleton
modified theorem lattice.Inf_univ
modified theorem lattice.Sup_empty
modified theorem lattice.Sup_insert
modified theorem lattice.Sup_singleton
modified theorem lattice.Sup_univ
modified theorem lattice.foo'
modified theorem lattice.foo
modified theorem lattice.infi_congr_Prop
modified theorem lattice.infi_const
modified theorem lattice.infi_empty
modified theorem lattice.infi_emptyset
modified theorem lattice.infi_exists
modified theorem lattice.infi_false
modified theorem lattice.infi_infi_eq_left
modified theorem lattice.infi_infi_eq_right
modified theorem lattice.infi_insert
modified theorem lattice.infi_le'
modified theorem lattice.infi_singleton
modified theorem lattice.infi_true
modified theorem lattice.infi_union
modified theorem lattice.infi_unit
modified theorem lattice.infi_univ
modified theorem lattice.le_Sup
modified theorem lattice.le_Sup_iff
modified theorem lattice.le_infi_iff
modified theorem lattice.le_supr'
modified theorem lattice.supr_congr_Prop
modified theorem lattice.supr_const
modified theorem lattice.supr_empty
modified theorem lattice.supr_emptyset
modified theorem lattice.supr_exists
modified theorem lattice.supr_false
modified theorem lattice.supr_insert
modified theorem lattice.supr_le_iff
modified theorem lattice.supr_singleton
modified theorem lattice.supr_supr_eq_left
modified theorem lattice.supr_supr_eq_right
modified theorem lattice.supr_true
modified theorem lattice.supr_union
modified theorem lattice.supr_unit
modified theorem lattice.supr_univ
modified theorem diff_empty
modified theorem filter.fmap_principal
modified theorem filter.inf_principal
modified theorem filter.infi_sets_induct
modified theorem filter.le_principal_iff
modified theorem filter.lift'_id
modified theorem filter.map_bot
modified theorem filter.map_compose
modified theorem filter.map_eq_bot_iff
modified theorem filter.map_id
modified theorem filter.map_principal
modified theorem filter.map_sup
modified theorem filter.mem_bot_sets
modified theorem filter.mem_inf_sets
modified theorem filter.mem_join_sets
modified theorem filter.mem_map
modified theorem filter.mem_principal_sets
modified theorem filter.mem_pure
modified theorem filter.mem_sup_sets
modified theorem filter.mem_top_sets_iff
modified theorem filter.principal_eq_bot_iff
modified theorem filter.principal_eq_iff_eq
modified theorem filter.sup_join
modified theorem filter.sup_principal
modified theorem filter.supr_join
modified theorem filter.supr_map
modified theorem filter.supr_principal
modified theorem filter.vmap_principal
modified theorem not_not_mem_iff
modified theorem prod.fst_swap
modified theorem prod.snd_swap
modified theorem prod.swap_prod_mk
modified theorem prod.swap_swap
modified theorem prod.swap_swap_eq
modified theorem set.prod_mk_mem_set_prod_eq
modified theorem set.set_of_mem_eq
modified theorem set.vimage_set_of_eq
modified theorem singleton_neq_emptyset
modified theorem bool.band_assoc
modified theorem bool.band_comm
modified theorem bool.band_elim_left
modified theorem bool.band_elim_right
modified theorem bool.band_eq_ff
modified theorem bool.band_eq_tt
modified theorem bool.band_ff
modified theorem bool.band_intro
modified theorem bool.band_left_comm
modified theorem bool.band_self
modified theorem bool.band_tt
modified theorem bool.bnot_bnot
modified theorem bool.bnot_false
modified theorem bool.bnot_true
modified theorem bool.bor_assoc
modified theorem bool.bor_comm
modified theorem bool.bor_eq_ff
modified theorem bool.bor_eq_tt
modified theorem bool.bor_ff
modified theorem bool.bor_inl
modified theorem bool.bor_inr
modified theorem bool.bor_left_comm
modified theorem bool.bor_tt
modified def bool.bxor
modified theorem bool.bxor_assoc
modified theorem bool.bxor_comm
modified theorem bool.bxor_ff
modified theorem bool.bxor_left_comm
modified theorem bool.bxor_self
modified theorem bool.bxor_tt
modified theorem bool.coe_tt
modified theorem bool.cond_ff
modified theorem bool.cond_tt
modified theorem bool.dichotomy
modified theorem bool.eq_ff_of_bnot_eq_tt
modified theorem bool.eq_ff_of_ne_tt
modified theorem bool.eq_tt_of_bnot_eq_ff
modified theorem bool.eq_tt_of_ne_ff
modified theorem bool.ff_band
modified theorem bool.ff_bor
modified theorem bool.ff_bxor
modified theorem bool.ff_bxor_ff
modified theorem bool.ff_bxor_tt
modified theorem bool.or_of_bor_eq
modified theorem bool.tt_band
modified theorem bool.tt_bor
modified theorem bool.tt_bxor
modified theorem bool.tt_bxor_ff
modified theorem bool.tt_bxor_tt
modified theorem list.append.assoc
modified theorem list.concat_append
modified theorem list.concat_ne_nil
modified theorem list.cons_ne_nil
modified theorem list.count_append
modified theorem list.count_concat
modified theorem list.count_cons_of_ne
modified theorem list.count_cons_self
modified theorem list.count_nil
modified theorem list.head_cons
modified theorem list.index_of_cons_of_eq
modified theorem list.index_of_cons_of_ne
modified theorem list.index_of_nil
modified theorem list.index_of_of_not_mem
modified theorem list.ith_succ
modified theorem list.ith_zero
modified theorem list.last_cons_cons
modified theorem list.last_singleton
modified theorem list.tail_cons
modified theorem list.tail_nil
modified theorem list.taken_nil
modified theorem list.taken_zero
modified theorem list.all_cons
modified theorem list.all_nil
modified theorem list.any_cons
modified theorem list.any_nil
modified theorem list.exists_mem_cons_iff
modified theorem list.foldl_append
modified theorem list.foldl_cons
modified theorem list.foldl_nil
modified theorem list.foldr_append
modified theorem list.foldr_cons
modified theorem list.foldr_nil
modified theorem list.forall_mem_cons_iff
modified theorem list.length_map_accumr
modified theorem list.length_map_accumr₂
modified theorem list.length_replicate
modified theorem list.unzip_cons
modified theorem list.unzip_nil
modified theorem list.zip_cons_cons
modified theorem list.zip_nil_left
modified theorem list.zip_nil_right
modified theorem list.perm.perm_app_comm
modified theorem list.perm.perm_induction_on
modified theorem list.perm.perm_map
modified theorem list.perm.perm_rev_simp
modified theorem list.erase_cons_head
modified theorem list.erase_cons_tail
modified theorem list.erase_nil
modified theorem list.erase_of_not_mem
modified theorem list.insert_nil
modified theorem list.insert_of_mem
modified theorem list.insert_of_not_mem
modified theorem list.inter_cons_of_mem
modified theorem list.inter_cons_of_not_mem
modified theorem list.inter_nil
modified theorem list.length_erase_of_mem
modified theorem list.length_insert_of_mem
modified theorem list.length_upto
modified theorem list.mem_erase_dup_iff
modified theorem list.mem_insert_iff
modified theorem list.mem_insert_of_mem
modified theorem list.mem_insert_self
modified theorem list.mem_inter_iff
modified theorem list.mem_union_iff
modified theorem list.union_cons
modified theorem list.union_nil
modified theorem list.upto_nil
modified theorem list.upto_succ
modified theorem nat.succ_add_eq_succ_add
modified theorem nat.dist_comm
modified theorem nat.dist_self
modified theorem set.insert_eq_of_mem
modified theorem set.mem_insert_iff
modified theorem set.mem_sep_eq
modified theorem set.finite_insert
modified theorem set.finite_singleton
modified def set.Inter
modified def set.Union
modified theorem set.bInter_empty
modified theorem set.bInter_insert
modified theorem set.bInter_singleton
modified theorem set.bInter_univ
modified theorem set.bUnion_empty
modified theorem set.bUnion_insert
modified theorem set.bUnion_singleton
modified theorem set.bUnion_univ
modified theorem set.insert_sdiff_singleton
modified theorem set.mem_Inter_eq
modified theorem set.mem_Union_eq
modified theorem set.mem_sInter_eq
modified theorem set.mem_sUnion_eq
modified def set.sInter
modified theorem set.sInter_empty
modified theorem set.sInter_image
modified theorem set.sInter_insert
modified theorem set.sInter_singleton
modified theorem set.sUnion_empty
modified theorem set.sUnion_image
modified theorem set.sUnion_insert
modified theorem set.sUnion_singleton
modified theorem set.sdiff_singleton_eq_same
modified theorem set.union_same_compl
modified theorem prod.exists
modified theorem prod.forall
modified theorem prod.mk.inj_iff
modified theorem set_of_subset_set_of
modified theorem mem_image
modified theorem mem_set_of
modified theorem false_neq_true
modified theorem open_singleton_true
modified theorem closed_closure
modified theorem closed_compl_iff_open
modified theorem closed_empty
modified theorem closed_univ
modified theorem closure_closure
modified theorem closure_compl_eq
modified theorem closure_empty
modified theorem closure_union
modified theorem closure_univ
modified theorem interior_compl_eq
modified theorem interior_empty
modified theorem interior_inter
modified theorem interior_interior
modified theorem interior_univ
modified theorem nhds_neq_bot
modified theorem open_compl_iff_closed
modified theorem open_empty
modified theorem open_interior
modified theorem open_univ