Mathlib Changelog
v3
Changelog
About
Github
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