Commit 2017-08-10 16:36 7882677d

View on Github →

construct reals as complete, linear ordered field

Estimated changes

added theorem abs_inv
added theorem inv_neg
added theorem inv_sub_inv_eq
added theorem ivl_stretch
added theorem ivl_translate
added theorem lt_div_iff
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_ultrafilter
modified theorem filter.filter_eq
modified theorem filter.fmap_principal
modified theorem filter.image_mem_map
modified theorem filter.inf_principal
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.inter_mem_sets
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'_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_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_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_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_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_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_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_pure
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
added theorem set.image_inter
added theorem set.image_singleton
modified theorem set.image_swap_prod
modified theorem set.mem_prod_eq
modified theorem set.mem_seq_iff
modified theorem set.ne_empty_iff_exists_mem
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.set_of_mem_eq
added theorem set.univ_eq_true_false
modified theorem singleton_neq_emptyset
added theorem not_le_iff
added theorem not_lt_iff
deleted def weak_order_dual
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 def rat.nat_ceil
added theorem rat.nat_ceil_min
added theorem rat.nat_ceil_mono
added theorem rat.nat_ceil_spec
added theorem rat.nat_ceil_zero
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
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
modified theorem continuous_subtype_mk
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.ext_eq
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_open
added theorem embedding_prod_mk
added theorem embedding_subtype_val
deleted theorem false_neq_true
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
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
deleted theorem univ_eq_true_false
added theorem univ_prod_univ
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 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 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 lt_mem_nhds
added theorem map_neg_rat
added theorem map_neg_real
added theorem mem_uniformity_rat
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_sub_rat'
added theorem towards_zero_nhds
added theorem two_eq_of_rat_two
added theorem uniform_continuous_rat
added theorem uniformity_rat
added theorem zero_le_iff_nonneg
added theorem zero_lt_two
added def zero_nhd
modified theorem closed_Inter
added theorem closed_Union
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_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_union
modified theorem closure_univ
modified def compact
modified theorem compact_adherence_nhdset
added theorem compact_empty
added theorem compact_singleton
added theorem diff_subset_diff
modified theorem eq_of_nhds_eq_nhds
modified theorem eq_of_nhds_neq_bot
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_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_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 sup_eq_generate_from
modified theorem supr_eq_generate_from
added theorem t2_separation
modified theorem t2_space_top
modified theorem topological_space_eq
added theorem towards_const_nhds
added theorem towards_nhds
added theorem towards_nhds_unique
added theorem univ_subtype
modified theorem Cauchy.monotone_gen
modified theorem Cauchy.pure_cauchy_dense
deleted def cauchy
modified theorem cauchy_downwards
modified theorem cauchy_map
modified theorem cauchy_nhds
modified theorem cauchy_pure
modified theorem cauchy_vmap
modified theorem closure_eq_inter_uniformity
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 complete_of_closed
modified theorem complete_space_extension
modified theorem complete_space_separation
modified theorem continuous_of_uniform
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 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
modified theorem to_topological_space_bot
modified theorem to_topological_space_mono
modified theorem to_topological_space_supr
modified theorem to_topological_space_top
modified theorem totally_bounded_iff_filter
added theorem totally_bounded_image
added theorem totally_bounded_subset
deleted def uniform_continuous
added theorem uniform_continuous_fst
added theorem uniform_continuous_snd
modified theorem uniform_continuous_vmap
deleted def uniform_embedding
added theorem uniform_embedding_prod
added theorem uniform_extend_subtype
added structure uniform_space.core
added theorem uniform_space.core_eq
modified theorem uniform_space_eq
modified def uniformity
modified theorem uniformity_eq_symm
modified theorem uniformity_le_symm
modified theorem uniformity_lift_le_comp
added theorem uniformity_prod
added theorem uniformity_subtype
modified theorem uniformly_extend_of_emb
modified theorem uniformly_extend_spec
deleted theorem uniformly_extend_unique
modified theorem vmap_quotient_le_uniformity