Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-10 09:32 fe1575a0

View on Github →

chore(topology): sanity_check pass (#1416)

  • chore(topology): sanity_check pass
  • improvement
  • avoid _inst_3 to recover instance

Estimated changes

modified theorem convex_on_sum
modified theorem ball_of_forall
modified theorem not_iff
added theorem antisymm_of_asymm
deleted def antisymm_of_asymm
modified theorem dense_or_discrete
modified theorem with_top.coe_ne_top
modified theorem with_top.top_ne_coe
modified theorem lattice.cInf_interval
modified theorem lattice.cSup_interval
added theorem filter.mem_pmap
deleted def filter.mem_pmap
added theorem filter.mem_rcomap'
deleted def filter.mem_rcomap'
modified theorem filter.liminf_le_liminf
modified theorem filter.liminf_le_limsup
modified theorem filter.limsup_le_limsup
deleted theorem order_embedding.nat_gt
deleted theorem order_embedding.nat_lt
deleted theorem order_iso.prod_lex_congr
deleted theorem order_iso.sum_lex_congr
added theorem nhds_is_mul_hom
deleted def nhds_is_mul_hom
modified theorem quotient_group_saturate
modified theorem has_sum_hom
modified theorem quotient_ring_saturate
modified theorem mem_closure
modified theorem tendsto_pure_nhds
modified theorem continuous_at_subtype_val
modified theorem dense_range_prod
modified theorem is_closed_diagonal
modified theorem is_closed_eq
modified theorem is_closed_prod
modified theorem is_closed_property
modified theorem list.continuous_at_length
modified theorem list.tendsto_cons
modified theorem list.tendsto_cons_iff
modified theorem list.tendsto_insert_nth
modified theorem list.tendsto_nhds
modified theorem mem_closure2
modified theorem normal_of_compact_t2
modified theorem prod_eq_generate_from
modified theorem tendsto_subtype_rng
deleted theorem dense_range.inhabited
modified theorem embedding.map_nhds_eq
added theorem embedding.mk'
deleted def embedding.mk'
modified theorem inducing.map_nhds_eq
modified theorem inducing.nhds_eq_comap
modified theorem subtype.dist_eq
modified theorem subtype.edist_eq
modified theorem induced_compose
modified theorem principal_subtype
modified theorem compact_image
modified theorem compact_of_closed
modified theorem compact_range
modified theorem compact_univ