Commit 2023-02-02 05:07 da8b9b6c

View on Github →

feat: port Topology.UniformSpace.Basic (#1993)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Filter/Bases.lean

Created Mathlib/Topology/UniformSpace/Basic.lean

added theorem Dense.bunionᵢ_uniformity_ball

added theorem Disjoint.exists_uniform_thickening

added theorem Disjoint.exists_uniform_thickening_of_basis

added theorem Filter.HasBasis.binterᵢ_bunionᵢ_ball

added theorem Filter.HasBasis.mem_uniformity_iff

added theorem Filter.HasBasis.uniformContinuousOn_iff

added theorem Filter.HasBasis.uniformContinuous_iff

added theorem Filter.HasBasis.uniformity_closure

added theorem Filter.Tendsto.congr_uniformity

added theorem Filter.Tendsto.uniformity_symm

added theorem Filter.Tendsto.uniformity_trans

added theorem IsCompact.nhdsSet_basis_uniformity

added theorem Monotone.compRel

added theorem MulOpposite.uniformContinuous_op

added theorem MulOpposite.uniformContinuous_unop

added theorem Sum.uniformity

added theorem SymmetricRel.eq

added theorem SymmetricRel.inter

added theorem SymmetricRel.mk_mem_comm

added def SymmetricRel

added theorem Uniform.continuousAt_iff'_left

added theorem Uniform.continuousAt_iff'_right

added theorem Uniform.continuousAt_iff_prod

added theorem Uniform.continuousOn_iff'_left

added theorem Uniform.continuousOn_iff'_right

added theorem Uniform.continuousWithinAt_iff'_left

added theorem Uniform.continuousWithinAt_iff'_right

added theorem Uniform.continuous_iff'_left

added theorem Uniform.continuous_iff'_right

added theorem Uniform.tendsto_congr

added theorem Uniform.tendsto_nhds_left

added theorem Uniform.tendsto_nhds_right

added theorem UniformContinuous.continuous

added theorem UniformContinuous.inf_dom_left

added theorem UniformContinuous.inf_dom_right

added theorem UniformContinuous.inf_rng

added theorem UniformContinuous.prod_map

added theorem UniformContinuous.prod_mk

added theorem UniformContinuous.prod_mk_left

added theorem UniformContinuous.prod_mk_right

added theorem UniformContinuous.subtype_mk

added def UniformContinuous

added theorem UniformContinuousOn.continuousOn

added def UniformContinuousOn

added theorem UniformContinuous₂.bicompl

added theorem UniformContinuous₂.comp

added theorem UniformContinuous₂.uniformContinuous

added def UniformContinuous₂

added def UniformSpace.Core.mk'

added def UniformSpace.Core.mkOfBasis

added def UniformSpace.Core.sum

added def UniformSpace.Core.toTopologicalSpace

added structure UniformSpace.Core

added def UniformSpace.ball

added theorem UniformSpace.ball_mem_nhds

added def UniformSpace.comap

added theorem UniformSpace.comap_comap

added theorem UniformSpace.comap_inf

added theorem UniformSpace.comap_infᵢ

added theorem UniformSpace.comap_mono

added theorem UniformSpace.core_eq

added theorem UniformSpace.hasBasis_nhds

added theorem UniformSpace.hasBasis_nhds_prod

added theorem UniformSpace.hasBasis_symmetric

added theorem UniformSpace.has_seq_basis

added theorem UniformSpace.isOpen_ball

added theorem UniformSpace.mem_ball_self

added theorem UniformSpace.mem_closure_iff_ball

added theorem UniformSpace.mem_closure_iff_symm_ball

added theorem UniformSpace.mem_nhds_iff

added theorem UniformSpace.mem_nhds_iff_symm

added def UniformSpace.mk'

added def UniformSpace.ofCore

added def UniformSpace.ofCoreEq

added theorem UniformSpace.ofCoreEq_toCore

added def UniformSpace.ofNhdsEqComap

added def UniformSpace.replaceTopology

added theorem UniformSpace.replaceTopology_eq

added theorem UniformSpace.toCore_toTopologicalSpace

added theorem ball_eq_of_symmetry

added theorem ball_inter

added theorem ball_inter_left

added theorem ball_inter_right

added theorem ball_mono

added theorem ball_subset_of_comp_subset

added theorem closure_eq_inter_uniformity

added theorem closure_eq_uniformity

added theorem comap_swap_uniformity

added theorem comap_uniformity_mulOpposite

added def compRel

added theorem compRel_assoc

added theorem compRel_mono

added theorem comp_comp_symm_mem_uniformity_sets

added theorem comp_le_uniformity3

added theorem comp_le_uniformity

added theorem comp_mem_uniformity_sets

added theorem comp_open_symm_mem_uniformity_sets

added theorem comp_symm_mem_uniformity_sets

added theorem comp_symm_of_uniformity

added theorem discreteTopology_of_discrete_uniformity

added theorem eventually_uniformity_comp_subset

added theorem eventually_uniformity_iterate_comp_subset

added theorem exists_mem_nhds_ball_subset_of_mem_nhds

added def idRel

added theorem idRel_subset

added theorem id_compRel

added theorem inf_uniformity

added theorem infᵢ_uniformity

added theorem interior_mem_uniformity

added theorem isOpen_iff_ball_subset

added theorem isOpen_iff_open_ball_subset

added theorem isOpen_uniformity

added theorem le_iff_uniformContinuous_id

added theorem lebesgue_number_lemma

added theorem lebesgue_number_lemma_unionₛ

added theorem lebesgue_number_of_compact_open

added theorem left_subset_compRel

added theorem lift_nhds_left

added theorem lift_nhds_right

added theorem map_uniformity_set_coe

added theorem mem_ball_comp

added theorem mem_ball_symmetry

added theorem mem_compRel

added theorem mem_comp_comp

added theorem mem_comp_of_mem_ball

added theorem mem_idRel

added theorem mem_nhds_left

added theorem mem_nhds_right

added theorem mem_nhds_uniformity_iff_left

added theorem mem_nhds_uniformity_iff_right

added theorem mem_uniform_prod

added theorem mem_uniformity_isClosed

added theorem mem_uniformity_of_eq

added theorem mem_uniformity_of_uniformContinuous_invariant

added theorem nhdsSet_diagonal_le_uniformity

added theorem nhds_basis_uniformity'

added theorem nhds_basis_uniformity

added theorem nhds_eq_comap_uniformity'

added theorem nhds_eq_comap_uniformity

added theorem nhds_eq_uniformity'

added theorem nhds_eq_uniformity

added theorem nhds_eq_uniformity_prod

added theorem nhds_le_uniformity

added theorem nhds_nhds_eq_uniformity_uniformity_prod

added theorem nhdset_of_mem_uniformity

added theorem open_of_uniformity_sum_aux

added theorem prod_mk_mem_compRel

added theorem refl_le_uniformity

added theorem refl_mem_uniformity

added theorem right_subset_compRel

added theorem subset_comp_self

added theorem subset_comp_self_of_mem_uniformity

added theorem subset_iterate_compRel

added theorem supᵢ_nhds_le_uniformity

added theorem swap_idRel

added theorem symm_le_uniformity

added theorem symm_of_uniformity

added theorem symmetric_symmetrizeRel

added def symmetrizeRel

added theorem symmetrizeRel_subset_self

added theorem symmetrize_mem_uniformity

added theorem symmetrize_mono

added theorem tendsto_const_uniformity

added theorem tendsto_diag_uniformity

added theorem tendsto_left_nhds_uniformity

added theorem tendsto_of_uniformContinuous_subtype

added theorem tendsto_prod_uniformity_fst

added theorem tendsto_prod_uniformity_snd

added theorem tendsto_right_nhds_uniformity

added theorem tendsto_swap_uniformity

added theorem toTopologicalSpace_bot

added theorem toTopologicalSpace_comap

added theorem toTopologicalSpace_inf

added theorem toTopologicalSpace_infᵢ

added theorem toTopologicalSpace_infₛ

added theorem toTopologicalSpace_mono

added theorem toTopologicalSpace_prod

added theorem toTopologicalSpace_subtype

added theorem toTopologicalSpace_top

added theorem to_nhds_mono

added theorem uniformContinuousOn_iff_restrict

added theorem uniformContinuousOn_univ

added theorem uniformContinuous_comap'

added theorem uniformContinuous_comap

added theorem uniformContinuous_const

added theorem uniformContinuous_def

added theorem uniformContinuous_fst

added theorem uniformContinuous_id

added theorem uniformContinuous_iff

added theorem uniformContinuous_iff_eventually

added theorem uniformContinuous_inf_dom_left₂

added theorem uniformContinuous_inf_dom_right₂

added theorem uniformContinuous_infᵢ_dom

added theorem uniformContinuous_infᵢ_rng

added theorem uniformContinuous_infₛ_dom

added theorem uniformContinuous_infₛ_dom₂

added theorem uniformContinuous_infₛ_rng

added theorem uniformContinuous_ofAdd

added theorem uniformContinuous_ofMul

added theorem uniformContinuous_of_const

added theorem uniformContinuous_snd

added theorem uniformContinuous_subtype_val

added theorem uniformContinuous_toAdd

added theorem uniformContinuous_toMul

added theorem uniformContinuous₂_curry

added theorem uniformContinuous₂_def

added theorem uniformSpace_comap_id

added theorem uniformSpace_eq

added def uniformity

added theorem uniformity_additive

added theorem uniformity_comap

added theorem uniformity_eq_symm

added theorem uniformity_eq_uniformity_closure

added theorem uniformity_eq_uniformity_interior

added theorem uniformity_hasBasis_closed

added theorem uniformity_hasBasis_closure

added theorem uniformity_hasBasis_open

added theorem uniformity_hasBasis_open_symmetric

added theorem uniformity_le_symm

added theorem uniformity_lift_le_comp

added theorem uniformity_lift_le_swap

added theorem uniformity_mulOpposite

added theorem uniformity_multiplicative

added theorem uniformity_prod

added theorem uniformity_prod_eq_comap_prod

added theorem uniformity_prod_eq_prod

added theorem uniformity_setCoe

added theorem uniformity_subtype

added theorem uniformity_sum_of_open_aux

added theorem union_mem_uniformity_sum