Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-08-10 16:36 7882677d

View on Github →

construct reals as complete, linear ordered field

Estimated changes

Created algebra/field.lean

added theorem abs_inv

added theorem div_le_iff_le_mul_of_pos

added theorem inv_neg

added theorem inv_sub_inv_eq

added theorem ivl_stretch

added theorem ivl_translate

added theorem le_div_iff_mul_le_of_pos

added theorem lt_div_iff

Modified algebra/group.lean

added theorem abs_le_iff

added theorem le_sub_iff_add_le

added theorem sub_le_iff_le_add

Modified algebra/lattice/complete_lattice.lean

added def ord_continuous

added theorem ord_continuous_mono

added theorem ord_continuous_sup

Modified algebra/lattice/filter.lean

modified theorem Union_subset_Union2

modified theorem Union_subset_Union

modified theorem Union_subset_Union_const

modified theorem bind_assoc

added theorem classical.cases

modified theorem compl_image_set_of

modified theorem diff_empty

modified theorem diff_neq_empty

modified theorem directed_on_Union

modified theorem eq_of_sup_eq_inf_eq

added theorem false_neq_true

modified theorem filter.Inf_sets_eq_finite

modified theorem filter.Inter_mem_sets

modified theorem filter.bind_def

modified theorem filter.bind_mono2

modified theorem filter.bind_mono

modified theorem filter.bind_sup

modified theorem filter.binfi_sup_eq

modified theorem filter.empty_in_sets_eq_bot

modified theorem filter.exists_sets_subset_iff

modified theorem filter.exists_ultrafilter

modified theorem filter.filter_eq

modified theorem filter.filter_eq_bot_of_not_nonempty

modified theorem filter.fmap_principal

modified theorem filter.forall_sets_neq_empty_iff_neq_bot

modified theorem filter.image_mem_map

modified theorem filter.inf_principal

modified theorem filter.infi_neq_bot_iff_of_directed

modified theorem filter.infi_neq_bot_of_directed

modified theorem filter.infi_sets_eq'

modified theorem filter.infi_sets_eq

modified theorem filter.infi_sets_induct

modified theorem filter.infi_sup_eq

modified theorem filter.inhabited_of_mem_sets

added theorem filter.inter_mem_inf_sets

modified theorem filter.inter_mem_sets

modified theorem filter.join_principal_eq_Sup

modified theorem filter.le_lift'

added theorem filter.le_map_vmap'

modified theorem filter.le_map_vmap

modified theorem filter.le_of_ultrafilter

modified theorem filter.le_principal_iff

modified theorem filter.le_vmap_iff_map_le

modified theorem filter.le_vmap_map

modified theorem filter.lift'_cong

modified theorem filter.lift'_id

modified theorem filter.lift'_inf_principal_eq

modified theorem filter.lift'_infi

added theorem filter.lift'_le

modified theorem filter.lift'_lift'_assoc

modified theorem filter.lift'_lift_assoc

modified theorem filter.lift'_mono'

modified theorem filter.lift'_mono

modified theorem filter.lift'_neq_bot_iff

modified theorem filter.lift'_principal

modified theorem filter.lift_assoc

modified theorem filter.lift_comm

modified theorem filter.lift_infi'

modified theorem filter.lift_infi

added theorem filter.lift_le

modified theorem filter.lift_lift'_assoc

modified theorem filter.lift_lift'_same_eq_lift'

modified theorem filter.lift_lift'_same_le_lift'

modified theorem filter.lift_lift_same_eq_lift

modified theorem filter.lift_lift_same_le_lift

modified theorem filter.lift_mono'

modified theorem filter.lift_mono

modified theorem filter.lift_neq_bot_iff

modified theorem filter.lift_principal

modified theorem filter.lift_sets_eq

modified theorem filter.map_binfi_eq

modified theorem filter.map_bot

modified theorem filter.map_compose

added theorem filter.map_cong

modified theorem filter.map_eq_bot_iff

modified theorem filter.map_eq_vmap_of_inverse

modified theorem filter.map_id

added theorem filter.map_inf

modified theorem filter.map_infi_eq

modified theorem filter.map_infi_le

added theorem filter.map_inj

modified theorem filter.map_lift'_eq2

modified theorem filter.map_lift'_eq

modified theorem filter.map_lift_eq2

modified theorem filter.map_lift_eq

added theorem filter.map_map

modified theorem filter.map_mono

added theorem filter.map_ne_bot

modified theorem filter.map_principal

modified theorem filter.map_sup

modified theorem filter.map_swap_vmap_swap_eq

modified theorem filter.map_vmap_le

modified theorem filter.mem_bind_sets

modified theorem filter.mem_bot_sets

modified theorem filter.mem_inf_sets

modified theorem filter.mem_inf_sets_of_left

modified theorem filter.mem_inf_sets_of_right

modified theorem filter.mem_infi_sets

modified theorem filter.mem_join_sets

modified theorem filter.mem_lift'

modified theorem filter.mem_lift'_iff

modified theorem filter.mem_lift

modified theorem filter.mem_lift_iff

modified theorem filter.mem_map

modified theorem filter.mem_of_finite_Union_ultrafilter

modified theorem filter.mem_of_finite_sUnion_ultrafilter

modified theorem filter.mem_or_compl_mem_of_ultrafilter

modified theorem filter.mem_or_mem_of_ultrafilter

modified theorem filter.mem_principal_sets

modified theorem filter.mem_prod_iff

modified theorem filter.mem_prod_same_iff

modified theorem filter.mem_pure

modified theorem filter.mem_return_sets

modified theorem filter.mem_sets_of_neq_bot

modified theorem filter.mem_sup_sets

modified theorem filter.mem_top_sets_iff

added theorem filter.mem_vmap

deleted theorem filter.mem_vmap_of_mem

modified theorem filter.monotone_map

modified theorem filter.monotone_mem_sets

modified theorem filter.monotone_principal

modified theorem filter.monotone_vmap

modified theorem filter.preimage_mem_vmap

modified theorem filter.principal_bind

modified theorem filter.principal_empty

modified theorem filter.principal_eq_bot_iff

modified theorem filter.principal_eq_iff_eq

modified theorem filter.principal_le_lift'

modified theorem filter.principal_mono

modified theorem filter.principal_univ

modified theorem filter.prod_comm

modified theorem filter.prod_inf_prod

modified theorem filter.prod_lift'_lift'

modified theorem filter.prod_lift_lift

modified theorem filter.prod_map_map_eq

modified theorem filter.prod_mem_prod

modified theorem filter.prod_mono

modified theorem filter.prod_neq_bot

modified theorem filter.prod_principal_principal

modified theorem filter.prod_same_eq

modified theorem filter.prod_vmap_vmap_eq

modified theorem filter.pure_def

modified theorem filter.return_neq_bot

modified theorem filter.seq_mono

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.supr_sets_eq

added theorem filter.towards_compose

added theorem filter.towards_cong

added theorem filter.towards_fst

added theorem filter.towards_id'

added theorem filter.towards_id

added theorem filter.towards_inf

added theorem filter.towards_map'

added theorem filter.towards_map

added theorem filter.towards_prod_mk

added theorem filter.towards_snd

added theorem filter.towards_vmap''

added theorem filter.towards_vmap'

added theorem filter.towards_vmap

modified theorem filter.ultrafilter_map

modified theorem filter.ultrafilter_of_le

modified theorem filter.ultrafilter_of_spec

modified theorem filter.ultrafilter_of_split

modified theorem filter.ultrafilter_of_ultrafilter

modified theorem filter.ultrafilter_pure

modified theorem filter.ultrafilter_ultrafilter_of

modified theorem filter.ultrafilter_unique

modified theorem filter.univ_mem_sets'

modified theorem filter.univ_mem_sets

added theorem filter.vmap_bot

added theorem filter.vmap_inf

added theorem filter.vmap_infi

modified theorem filter.vmap_lift_eq

modified theorem filter.vmap_map

modified theorem filter.vmap_mono

modified theorem filter.vmap_neq_bot

modified theorem filter.vmap_neq_bot_of_surj

added theorem filter.vmap_sup

modified theorem filter.vmap_vmap_comp

modified theorem implies_implies_true_iff

modified theorem inf_eq_bot_iff_le_compl

modified theorem lattice.Inf_eq_finite_sets

modified theorem map_bind

modified theorem neg_subset_neg_iff_subset

modified theorem not_not_mem_iff

added theorem not_or_iff_implies

modified theorem prod.fst_swap

modified theorem prod.mk.eta

modified theorem prod.snd_swap

modified theorem prod.swap_prod_mk

modified theorem prod.swap_swap

modified theorem prod.swap_swap_eq

modified theorem pure_seq_eq_map

modified theorem sUnion_eq_Union

modified theorem sUnion_mono

modified theorem seq_bind_eq

modified theorem seq_eq_bind_map

modified theorem set.bind_def

modified theorem set.diff_right_antimono

modified theorem set.fmap_eq_image

added theorem set.image_Union

deleted theorem set.image_eq_preimage_of_inverse

added theorem set.image_inter

added theorem set.image_singleton

modified theorem set.image_swap_prod

deleted theorem set.mem_image_iff_of_inverse

modified theorem set.mem_prod_eq

modified theorem set.mem_seq_iff

modified theorem set.ne_empty_iff_exists_mem

added theorem set.not_eq_empty_iff_exists

modified theorem set.prod_image_image_eq

modified theorem set.prod_inter_prod

modified theorem set.prod_mk_mem_set_prod_eq

modified theorem set.prod_mono

modified theorem set.prod_neq_empty_iff

modified theorem set.prod_singleton_singleton

modified theorem set.set_of_mem_eq

added theorem set.univ_eq_true_false

modified theorem singleton_neq_emptyset

Modified algebra/order.lean

added theorem not_le_iff

added theorem not_lt_iff

added def partial_order_dual

deleted def weak_order_dual

Modified algebra/ring.lean

Modified data/int/order.lean

added theorem int.le_of_of_nat_le_of_nat

added theorem int.of_nat_le_of_nat_of_le

Modified data/nat/basic.lean

added theorem nat.le_add_one_iff

added theorem nat.le_zero_iff

Modified data/rat.lean

added theorem rat.coe_int_add

added theorem rat.coe_int_eq_mk

added theorem rat.coe_int_one

added theorem rat.coe_int_sub

added theorem rat.coe_nat_rat_eq_mk

added theorem rat.exists_upper_nat_bound

added theorem rat.le_of_of_int_le_of_int

added def rat.nat_ceil

added theorem rat.nat_ceil_add_one_eq

added theorem rat.nat_ceil_lt_add_one

added theorem rat.nat_ceil_min

added theorem rat.nat_ceil_mono

added theorem rat.nat_ceil_spec

added theorem rat.nat_ceil_zero

Modified data/set/basic.lean

added theorem set.image_eq_preimage_of_inverse

added theorem set.mem_image_iff_of_inverse

added theorem set.mem_of_eq_of_mem

added theorem set.set_compr_eq_eq_singleton

modified theorem set.subset.trans

Modified data/set/finite.lean

added theorem set.finite_le_nat

Modified data/set/lattice.lean

added theorem set.monotone_image

Modified topology/continuity.lean

deleted theorem classical.cases

added theorem closed_diagonal

added theorem closed_eq

added theorem closed_prod

added theorem closed_property2

added theorem closed_property3

added theorem closed_property

added theorem closure_induced

modified theorem closure_prod_eq

added theorem closure_subtype

added theorem compact_image

modified theorem compact_pi_infinite

modified theorem continuous_Inf_dom

modified theorem continuous_Inf_rng

modified theorem continuous_Prop

modified theorem continuous_bot

modified theorem continuous_coinduced_dom

modified theorem continuous_coinduced_rng

modified theorem continuous_compose

added theorem continuous_const

modified theorem continuous_eq_le_coinduced

modified theorem continuous_fst

modified theorem continuous_id

added theorem continuous_iff_closed

modified theorem continuous_iff_induced_le

added theorem continuous_iff_of_embedding

modified theorem continuous_iff_towards

modified theorem continuous_induced_dom

modified theorem continuous_induced_rng

modified theorem continuous_inf_dom

modified theorem continuous_inf_rng_left

modified theorem continuous_inf_rng_right

modified theorem continuous_infi_dom

modified theorem continuous_infi_rng

modified theorem continuous_inl

modified theorem continuous_inr

modified theorem continuous_prod_mk

modified theorem continuous_snd

added theorem continuous_subtype_closed_cover

modified theorem continuous_subtype_mk

modified theorem continuous_subtype_nhds_cover

modified theorem continuous_subtype_val

modified theorem continuous_sum_rec

modified theorem continuous_sup_dom_left

modified theorem continuous_sup_dom_right

modified theorem continuous_sup_rng

modified theorem continuous_top

added theorem dense_embedding.closure_image_univ

added theorem dense_embedding.continuous_ext

added def dense_embedding.ext

added theorem dense_embedding.ext_e_eq

added theorem dense_embedding.ext_eq

added theorem dense_embedding.inj_iff

added def dense_embedding.subtype_emb

added theorem dense_embedding.towards_ext

added theorem dense_embedding.vmap_nhds_neq_bot

added structure dense_embedding

added def embedding

added theorem embedding_closed

added theorem embedding_compose

added theorem embedding_graph

added theorem embedding_id

added theorem embedding_of_embedding_compose

added theorem embedding_open

added theorem embedding_prod_mk

added theorem embedding_subtype_val

deleted theorem false_neq_true

added theorem image_closure_subset_closure_image

added theorem image_preimage_eq_inter_rng

added theorem induced_compose

added theorem induced_id

added theorem induced_mono

added theorem induced_sup

modified theorem map_nhds_induced_eq

modified theorem map_nhds_subtype_val_eq

added theorem mem_closure_of_continuous2

added theorem mem_closure_of_continuous

modified theorem nhds_induced_eq_vmap

modified theorem nhds_pi

modified theorem nhds_prod_eq

added theorem nhds_subtype_eq_vmap

modified theorem open_set_prod

modified theorem open_singleton_true

modified theorem prod_eq_generate_from

modified theorem subtype.val_image

added theorem towards_nhds_iff_of_embedding

deleted theorem univ_eq_true_false

added theorem univ_prod_univ

Created topology/real.lean

added theorem abs_real_eq_abs

added theorem closed_ge

added theorem closed_imp

added theorem closed_le

added theorem closed_le_real

added theorem closure_of_rat_image_eq

added theorem compact_ivl

added theorem continuous_abs_rat

added theorem continuous_abs_real

added theorem continuous_add_rat

added theorem continuous_add_real'

added theorem continuous_add_real

added theorem continuous_inv_real'

added theorem continuous_inv_real

added theorem continuous_mul_real'

added theorem continuous_mul_real

added theorem continuous_neg_rat

added theorem continuous_neg_real

added theorem continuous_sub_real

added theorem dense_embedding_of_rat

added theorem dense_embedding_of_rat_of_rat

added theorem eq_0_of_nonneg_of_neg_nonneg

added theorem exists_lt_of_rat

added theorem exists_supremum_real

added theorem forall_subtype_iff

added theorem gt_mem_nhds

added def lift_rat_fun

added theorem lift_rat_fun_of_rat

added def lift_rat_op

added theorem lift_rat_op_of_rat_of_rat

added theorem lt_mem_nhds

added theorem map_neg_rat

added theorem map_neg_real

added theorem mem_nonneg_of_continuous2

added theorem mem_uniformity_rat

added theorem mem_uniformity_real_iff

added theorem mem_zero_nhd

added theorem mem_zero_nhd_iff

added theorem neg_preimage_closure

added theorem nhds_0_eq_zero_nhd

added theorem nhds_eq_map_zero_nhd

added def nonneg

added def of_rat

added theorem of_rat_abs

added theorem of_rat_add

added theorem of_rat_inv

added theorem of_rat_le_of_rat

added theorem of_rat_lt_of_rat

added theorem of_rat_mem_nonneg

added theorem of_rat_mem_nonneg_iff

added theorem of_rat_mul

added theorem of_rat_neg

added theorem of_rat_one

added theorem of_rat_sub

added theorem of_rat_zero

added theorem one_lt_two

added theorem open_gt

added theorem open_lt

added theorem open_lt_real

added theorem preimage_neg_rat

added theorem preimage_neg_real

added theorem pure_zero_le_zero_nhd

added theorem quot_mk_image_univ_eq

added def real

added theorem totally_bounded_01_rat

added theorem towards_add_rat

added theorem towards_add_rat_zero'

added theorem towards_add_rat_zero

added theorem towards_inv_pos_rat

added theorem towards_inv_rat

added theorem towards_inv_real

added theorem towards_mul_bnd_rat'

added theorem towards_mul_bnd_rat

added theorem towards_mul_rat'

added theorem towards_mul_rat

added theorem towards_neg_rat

added theorem towards_neg_rat_zero

added theorem towards_of_uniform_continuous_subtype

added theorem towards_sub_rat'

added theorem towards_sub_uniformity_zero_nhd'

added theorem towards_sub_uniformity_zero_nhd

added theorem towards_zero_nhds

added theorem two_eq_of_rat_two

added theorem uniform_continuous_abs_rat

added theorem uniform_continuous_abs_real

added theorem uniform_continuous_add_rat

added theorem uniform_continuous_add_real

added theorem uniform_continuous_inv_pos_rat

added theorem uniform_continuous_mul_rat

added theorem uniform_continuous_neg_rat

added theorem uniform_continuous_neg_real

added theorem uniform_continuous_rat'

added theorem uniform_continuous_rat

added theorem uniform_embedding_add_rat

added theorem uniform_embedding_mul_rat

added theorem uniform_embedding_of_rat

added theorem uniformity_rat

added theorem zero_le_iff_nonneg

added theorem zero_lt_two

added def zero_nhd

Modified topology/topological_space.lean

modified theorem closed_Inter

added theorem closed_Union

modified theorem closed_Union_of_locally_finite

modified theorem closed_closure

added theorem closed_compl_iff

deleted theorem closed_compl_iff_open

modified theorem closed_empty

modified theorem closed_iff_nhds

added theorem closed_induced_iff

added theorem closed_inter

modified theorem closed_sInter

added theorem closed_singleton

modified theorem closed_union

modified theorem closed_univ

modified theorem closure_closure

modified theorem closure_compl_eq

added theorem closure_diff

modified theorem closure_empty

modified theorem closure_eq_compl_interior_compl

modified theorem closure_eq_iff_closed

modified theorem closure_eq_nhds

modified theorem closure_eq_of_closed

added theorem closure_inter_open

modified theorem closure_minimal

modified theorem closure_mono

added theorem closure_singleton

modified theorem closure_subset_iff_subset_of_closed

modified theorem closure_union

modified theorem closure_univ

modified def compact

modified theorem compact_adherence_nhdset

added theorem compact_elim_finite_subcover

added theorem compact_elim_finite_subcover_image

added theorem compact_empty

added theorem compact_iff_finite_subcover

modified theorem compact_iff_ultrafilter_le_nhds

added theorem compact_of_closed_subset

added theorem compact_of_finite_subcover

added theorem compact_singleton

added theorem compl_singleton_mem_nhds

added theorem compl_subset_of_compl_subset

added theorem diff_subset_diff

modified theorem eq_of_nhds_eq_nhds

modified theorem eq_of_nhds_neq_bot

deleted theorem finite_subcover_of_compact

modified theorem generate_from_le

modified theorem interior_compl_eq

modified theorem interior_empty

modified theorem interior_eq_iff_open

modified theorem interior_eq_nhds

modified theorem interior_eq_of_open

modified theorem interior_inter

modified theorem interior_interior

modified theorem interior_maximal

modified theorem interior_mono

modified theorem interior_subset

modified theorem interior_subset_closure

modified theorem interior_union_closed_of_interior_empty

modified theorem interior_univ

modified theorem le_of_nhds_le_nhds

added theorem lim_eq

added theorem lim_nhds_eq

added theorem lim_nhds_eq_of_closure

added theorem lim_spec

added theorem locally_finite_of_finite

added theorem locally_finite_subset

modified theorem map_nhds

modified theorem mem_nhds_sets

modified theorem mem_nhds_sets_iff

added theorem mem_of_mem_of_subset

added theorem mem_of_nhds

added theorem nhds_closed

added theorem nhds_eq_nhds_iff

added theorem nhds_le_nhds_iff

modified theorem nhds_mono

modified theorem nhds_neq_bot

modified theorem nhds_sets

modified theorem nhds_supr

added theorem not_and_iff_imp_not

deleted theorem not_eq_empty_iff_exists

modified theorem open_Union

added theorem open_compl_iff

deleted theorem open_compl_iff_closed

modified theorem open_diff

modified theorem open_empty

modified theorem open_iff_nhds

modified theorem open_inter

modified theorem open_interior

modified theorem open_sUnion

added theorem open_union

modified theorem open_univ

modified theorem return_le_nhds

modified theorem subset_closure

modified theorem subset_interior_iff_subset_of_open

modified theorem sup_eq_generate_from

modified theorem supr_eq_generate_from

added theorem t2_separation

modified theorem t2_space_top

modified theorem topological_space.nhds_generate_from

modified theorem topological_space_eq

added theorem towards_const_nhds

added theorem towards_nhds

added theorem towards_nhds_unique

added theorem univ_subtype

Modified topology/uniform_space.lean

modified theorem Cauchy.monotone_gen

modified theorem Cauchy.pure_cauchy_dense

modified theorem Cauchy.uniform_embedding_pure_cauchy

deleted def cauchy

modified theorem cauchy_downwards

modified theorem cauchy_map

modified theorem cauchy_nhds

modified theorem cauchy_of_totally_bounded_of_ultrafilter

modified theorem cauchy_pure

modified theorem cauchy_vmap

modified theorem closure_eq_inter_uniformity

added theorem closure_image_mem_nhds_of_uniform_embedding

modified theorem comp_le_uniformity3

modified theorem comp_le_uniformity

modified theorem comp_mem_uniformity_sets

modified def comp_rel

modified theorem comp_symm_of_uniformity

modified theorem compact_of_totally_bounded_closed

modified theorem compact_of_totally_bounded_complete

modified theorem complete_of_closed

modified theorem complete_space_extension

modified theorem complete_space_separation

modified theorem continuous_of_uniform

added theorem dense_embedding_of_uniform_embedding

added theorem forall_quotient_iff

modified theorem id_comp_rel

modified theorem interior_mem_uniformity

modified theorem le_nhds_iff_adhp_of_cauchy

modified theorem le_nhds_of_cauchy_adhp

modified theorem lift_nhds_left

modified theorem lift_nhds_right

modified theorem mem_nhds_left

modified theorem mem_nhds_right

modified theorem mem_nhds_uniformity_iff

added theorem mem_uniform_prod

added theorem mem_uniformity_closed

modified theorem nhds_eq_uniformity

modified theorem nhds_eq_uniformity_prod

modified theorem nhds_nhds_eq_uniformity_uniformity_prod

modified theorem nhdset_of_mem_uniformity

added theorem open_uniformity

modified theorem prod_mk_mem_comp_rel

modified theorem refl_le_uniformity

modified theorem refl_mem_uniformity

deleted def separated

modified theorem separated_equiv

added theorem separated_separation

added theorem sup_uniformity

modified theorem supr_uniformity

modified theorem symm_le_uniformity

modified theorem symm_of_uniformity

added theorem to_topological_space_Sup

modified theorem to_topological_space_bot

modified theorem to_topological_space_mono

added theorem to_topological_space_prod

added theorem to_topological_space_subtype

added theorem to_topological_space_sup

modified theorem to_topological_space_supr

modified theorem to_topological_space_top

added theorem totally_bounded_closure

modified theorem totally_bounded_iff_filter

modified theorem totally_bounded_iff_ultrafilter

added theorem totally_bounded_image

added theorem totally_bounded_subset

added theorem towards_const_uniformity

added theorem towards_left_nhds_uniformity

added theorem towards_prod_uniformity_fst

added theorem towards_prod_uniformity_snd

added theorem towards_right_nhds_uniformity

added theorem towards_swap_uniformity

deleted def uniform_continuous

added theorem uniform_continuous_compose

added theorem uniform_continuous_const

added theorem uniform_continuous_fst

modified theorem uniform_continuous_of_embedding

added theorem uniform_continuous_prod_mk

modified theorem uniform_continuous_quotient_mk

added theorem uniform_continuous_snd

added theorem uniform_continuous_subtype_mk

added theorem uniform_continuous_subtype_val

modified theorem uniform_continuous_uniformly_extend

added theorem uniform_continuous_vmap'

modified theorem uniform_continuous_vmap

deleted def uniform_embedding

added theorem uniform_embedding_prod

added theorem uniform_embedding_subtype_emb

added theorem uniform_extend_subtype

added def uniform_space.core.to_topological_space

added structure uniform_space.core

added theorem uniform_space.core_eq

added def uniform_space.of_core

added def uniform_space.of_core_eq

added theorem uniform_space.of_core_eq_to_core

added theorem uniform_space.to_core_to_topological_space

modified theorem uniform_space_eq

modified def uniformity

modified theorem uniformity_eq_symm

modified theorem uniformity_eq_uniformity_closure

modified theorem uniformity_eq_uniformity_interior

modified theorem uniformity_le_symm

modified theorem uniformity_lift_le_comp

added theorem uniformity_prod

added theorem uniformity_subtype

added theorem uniformly_extend_exists

modified theorem uniformly_extend_of_emb

modified theorem uniformly_extend_spec

deleted theorem uniformly_extend_unique

added theorem vmap_quotient_eq_uniformity

modified theorem vmap_quotient_le_uniformity