Cauchy

📁 Source: Mathlib/Topology/UniformSpace/Cauchy.lean

Statistics

Metric	Count
Definitions Cauchy, Cauchy, CauchySeq, CompleteSpace, cauchyConst, IsComplete, seq, setSeq, setSeqAux, interUnionBalls	10
Theorems comap, comap', le_nhds_lim, map, map_of_le, mono, mono', mono_uniformSpace, prod, ultrafilter_of, comp_injective, comp_tendsto, eventually_eventually, mem_entourage, nonempty, prodMap, prodMk, subseq_mem, subseq_subseq_mem, tendsto_limUnder, tendsto_uniformity, totallyBounded_range, addOpposite, complete, fst_of_prod, mulOpposite, prod, snd_of_prod, eq_pure_cauchyConst, eq_pure_of_cauchy, instCompleteSpace, cauchySeq_iff, cauchySeq_iff', cauchy_iff, filter_totallyBounded_iff, totallyBounded_iff, cauchySeq, cauchy_map, subseq_mem_entourage, exists_clusterPt, exists_subset_of_mem, isCompact_setOf_clusterPt, map, mono, sup, totallyBounded_setOf_clusterPt, totallyBounded_biSup, totallyBounded_bot, totallyBounded_iSup, totallyBounded_iff_filter, totallyBounded_iff_ultrafilter, totallyBounded_principal_iff, totallyBounded_sup, cauchySeq_comp_iff, isComplete, isComplete, totallyBounded, union, le_nhds_of_seq_tendsto_nhds, seq_is_cauchySeq, seq_mem, seq_pair_mem, setSeq_mem, setSeq_mono, setSeq_prod_subset, setSeq_sub_aux, totallyBounded, totallyBounded, closure, exists_subset, image, insert, isCompact_of_isClosed, isCompact_of_isComplete, isSeparable, subset, union, cauchy_of_totallyBounded, cauchy_of_totallyBounded', comp_cauchySeq, complete_of_cauchySeq_tendsto, complete_of_convergent_controlled_sequences, firstCountableTopology, secondCountable_of_almost_dense_set, secondCountable_of_separable, subset_countable_closure_of_almost_dense_set, cauchySeq_const, cauchySeq_iff, cauchySeq_iff', cauchySeq_iff_tendsto, cauchySeq_of_controlled, cauchySeq_shift, cauchySeq_tendsto_of_complete, cauchySeq_tendsto_of_isComplete, cauchy_comap_uniformSpace, cauchy_iInf_uniformSpace, cauchy_iInf_uniformSpace', cauchy_iff, cauchy_iff', cauchy_iff_exists_le_nhds, cauchy_iff_le, cauchy_inf_uniformSpace, cauchy_map_iff, cauchy_map_iff', cauchy_map_iff_exists_tendsto, cauchy_nhds, cauchy_prod_iff, cauchy_pure, completeSpace_iff_isComplete_univ, completeSpace_iff_ultrafilter, completeSpace_of_isComplete_univ, completeSpace_prod_of_nonempty, complete_of_compact, complete_univ, isCompact_closure_interUnionBalls, isCompact_iff_totallyBounded_isComplete, isComplete_iUnion_separated, isComplete_iff_clusterPt, isComplete_iff_ultrafilter, isComplete_iff_ultrafilter', le_nhds_iff_adhp_of_cauchy, le_nhds_of_cauchy_adhp, le_nhds_of_cauchy_adhp_aux, tendsto_nhds_of_cauchySeq_of_subseq, totallyBounded_biUnion, totallyBounded_closure, totallyBounded_empty, totallyBounded_iUnion, totallyBounded_iff_filter, totallyBounded_iff_subset, totallyBounded_iff_ultrafilter, totallyBounded_insert, totallyBounded_interUnionBalls, totallyBounded_of_forall_isSymm, totallyBounded_sSup, totallyBounded_sUnion, totallyBounded_singleton, totallyBounded_union	138
Total	148

CauSeq.Completion

Definitions

Name	Category	Theorems
Cauchy 📖	CompOp	53 math math: ofRat_div, ofRat_inv, ofRat_mul, ofRat_ratCast, Real.ofCauchy_zero, Real.ofCauchy_mul, Real.cauchy_sub, Real.ofCauchy_nnratCast, ofRat_rat, Real.ofCauchy_sub, ofRat_one, Real.cauchy_inv, Real.cauchy_nnratCast, mk_smul, ofRat_add, Real.ofCauchy_natCast, inv_mk, mk_add, Real.cauchy_natCast, Real.ofCauchy_ratCast, Real.ofCauchy_intCast, Real.ofCauchy_div, ofRat_sub, mk_mul, ofRat_nnratCast, Real.cauchy_neg, inv_zero, mul_inv_cancel, Real.cauchy_intCast, inv_mul_cancel, ofRat_zero, Real.cauchy_add, Real.ofCauchy_add, Real.ofCauchy_inv, Real.cauchy_zero, Real.ofCauchy_neg, Real.ofCauchy_one, Real.cauchy_one, ofRat_injective, Real.cauchy_ratCast, mk_neg, Real.cauchy_mul, ofRatRingHom_apply, Real.ringEquivCauchy_apply, mk_eq_zero, mk_pow, ofRat_intCast, mk_sub, Real.ringEquivCauchy_symm_apply_cauchy, ofRat_natCast, PadicSeq.eq_zero_iff_equiv_zero, Cauchy.instNonTrivial, ofRat_neg

Cauchy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap 📖	mathematical	Cauchy Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.comap uniformity	Cauchy Filter.comap	—	Filter.prod_comap_comap_eq Filter.comap_mono
comap' 📖	mathematical	Cauchy Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.comap uniformity	Cauchy Filter.comap	—	comap
le_nhds_lim 📖	mathematical	Cauchy	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds UniformSpace.toTopologicalSpace Filter.lim Filter.NeBot.nonempty Filter.NeBot SProd.sprod Filter.instSProd uniformity	—	le_nhds_lim CompleteSpace.complete
map 📖	mathematical	Cauchy UniformContinuous	Cauchy Filter.map	—	Filter.NeBot.map Filter.prod_map_map_eq Filter.map_mono
map_of_le 📖	mathematical	Cauchy UniformContinuousOn Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.principal	Cauchy Filter.map	—	comap' Filter.comap_coe_neBot_of_le_principal Filter.subtype_coe_map_comap inf_eq_left map UniformContinuousOn.restrict
mono 📖	mathematical	Cauchy Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder	Cauchy	—	le_trans Filter.prod_mono
mono' 📖	mathematical	Cauchy Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder	Cauchy	—	mono
mono_uniformSpace 📖	mathematical	UniformSpace Preorder.toLE PartialOrder.toPreorder instPartialOrderUniformSpace Cauchy	Cauchy	—	LE.le.trans
prod 📖	mathematical	Cauchy	Cauchy instUniformSpaceProd SProd.sprod Filter Filter.instSProd	—	Filter.map_fst_prod Filter.map_snd_prod
ultrafilter_of 📖	mathematical	Cauchy	Cauchy Ultrafilter.toFilter Ultrafilter.of Filter.NeBot Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder SProd.sprod Filter.instSProd uniformity	—	Ultrafilter.of_le Ultrafilter.neBot LE.le.trans Filter.prod_mono

CauchySeq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_injective 📖	mathematical	CauchySeq Nat.instPreorder	CauchySeq PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	comp_tendsto Filter.Tendsto.mono_left Function.Injective.tendsto_cofinite Filter.atTop_le_cofinite instNoTopOrderOfNoMaxOrder Nat.cofinite_eq_atTop
comp_tendsto 📖	mathematical	CauchySeq Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeSup.toPartialOrder	CauchySeq PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	Filter.map_neBot Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder le_trans Filter.prod_le_prod Filter.Tendsto.comp le_rfl
eventually_eventually 📖	mathematical	CauchySeq SetRel Filter Filter.instMembership uniformity	Filter.Eventually SetRel Set.instMembership Filter.atTop	—	Filter.eventually_atTop_curry tendsto_uniformity
mem_entourage 📖	mathematical	CauchySeq PartialOrder.toPreorder SemilatticeSup.toPartialOrder SetRel Filter Filter.instMembership uniformity	SetRel Set.instMembership	—	tendsto_uniformity Filter.HasBasis.tendsto_left_iff Filter.HasBasis.prod_self Filter.atTop_basis SemilatticeSup.instIsDirectedOrder nonempty Filter.prod_atTop_atTop_eq
nonempty 📖	—	CauchySeq	—	—	Filter.nonempty_of_neBot Filter.map_neBot_iff
prodMap 📖	mathematical	CauchySeq	CauchySeq instUniformSpaceProd Prod.instPreorder	—	Filter.prod_map_map_eq' Filter.prod_atTop_atTop_eq Cauchy.prod
prodMk 📖	mathematical	CauchySeq	CauchySeq instUniformSpaceProd	—	Cauchy.mono Filter.map_neBot Filter.NeBot.of_map Cauchy.prod Filter.Tendsto.prodMk Filter.tendsto_map
subseq_mem 📖	mathematical	SetRel Filter Filter.instMembership uniformity CauchySeq Nat.instPreorder	StrictMono Nat.instPreorder SetRel Set.instMembership	—	cauchySeq_iff le_trans Filter.extraction_forall_of_eventually' LT.lt.le
subseq_subseq_mem 📖	mathematical	SetRel Filter Filter.instMembership uniformity CauchySeq Nat.instPreorder Filter.Tendsto Filter.atTop	StrictMono Nat.instPreorder SetRel Set.instMembership	—	Filter.Tendsto.subseq_mem Filter.Tendsto.comp cauchySeq_iff_tendsto Filter.Tendsto.prod_atTop Filter.tendsto_atTop_diagonal
tendsto_limUnder 📖	mathematical	CauchySeq	Filter.Tendsto Filter.atTop nhds UniformSpace.toTopologicalSpace Filter.limUnder Filter.NeBot.nonempty Filter.map Filter.NeBot Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder SProd.sprod Filter.instSProd uniformity	—	Cauchy.le_nhds_lim
tendsto_uniformity 📖	mathematical	CauchySeq	Filter.Tendsto Filter.atTop Prod.instPreorder uniformity	—	Filter.prod_map_map_eq' Filter.prod_atTop_atTop_eq
totallyBounded_range 📖	mathematical	CauchySeq Nat.instPreorder	TotallyBounded Set.range	—	cauchySeq_iff Set.Finite.image Set.finite_le_nat Set.range_subset_iff Set.biUnion_image Set.mem_iUnion₂ le_total refl_mem_uniformity le_refl le_rfl

CompleteSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addOpposite 📖	mathematical	—	CompleteSpace AddOpposite instUniformSpaceAddOpposite	—	Function.Surjective.exists AddOpposite.op_surjective complete Cauchy.map AddOpposite.uniformContinuous_unop LE.le.trans_eq Filter.map_le_iff_le_comap AddOpposite.comap_unop_nhds
complete 📖	mathematical	Cauchy	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds UniformSpace.toTopologicalSpace	—	—
fst_of_prod 📖	mathematical	—	CompleteSpace	—	complete Cauchy.prod cauchy_pure Filter.map_fst_prod Filter.pure_neBot nhds_prod_eq nhds_neBot Filter.map_mono
mulOpposite 📖	mathematical	—	CompleteSpace MulOpposite instUniformSpaceMulOpposite	—	Function.Surjective.exists MulOpposite.op_surjective complete Cauchy.map MulOpposite.uniformContinuous_unop LE.le.trans_eq Filter.map_le_iff_le_comap MulOpposite.comap_unop_nhds
prod 📖	mathematical	—	CompleteSpace instUniformSpaceProd	—	complete Cauchy.map uniformContinuous_fst uniformContinuous_snd nhds_prod_eq Filter.le_prod
snd_of_prod 📖	mathematical	—	CompleteSpace	—	complete Cauchy.prod cauchy_pure Filter.map_snd_prod Filter.pure_neBot nhds_prod_eq nhds_neBot Filter.map_mono

DiscreteUniformity

Definitions

Name	Category	Theorems
cauchyConst 📖	CompOp	1 math math: eq_pure_cauchyConst

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_pure_cauchyConst 📖	mathematical	Cauchy	Filter Filter.instPure cauchyConst	—	eq_pure_of_cauchy
eq_pure_of_cauchy 📖	mathematical	Cauchy	Filter Filter.instPure	—	eq_principal_setRelId SetRel.exists_eq_singleton_of_prod_subset_id Filter.NeBot.nonempty_of_mem Filter.NeBot.le_pure_iff Filter.le_pure_iff
instCompleteSpace 📖	mathematical	—	CompleteSpace	—	eq_pure_of_cauchy pure_le_nhds

Filter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
totallyBounded_biSup 📖	mathematical	—	TotallyBounded iSup Filter instSupSet Set Set.instMembership	—	Set.Finite.to_subtype iSup_subtype' totallyBounded_iSup
totallyBounded_bot 📖	mathematical	—	TotallyBounded Bot.bot Filter instBot	—	principal_empty totallyBounded_principal_iff totallyBounded_empty
totallyBounded_iSup 📖	mathematical	—	TotallyBounded iSup Filter instSupSet	—	TotallyBounded.mono le_iSup Set.finite_iUnion SetRel.preimage_iUnion iSup_mono
totallyBounded_iff_filter 📖	mathematical	—	TotallyBounded Filter Preorder.toLE PartialOrder.toPreorder instPartialOrder Cauchy	—	Ultrafilter.of_le Ultrafilter.cauchy_of_totallyBounded' TotallyBounded.mono LE.le.trans Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq Mathlib.Tactic.Push.not_forall_eq inf_le_inf le_refl Set.compl_subset_compl_of_subset SetRel.preimage_subset_preimage iInf_neBot_iff_of_directed' Antitone.directed_ge Finset.isDirected_le notMem_iff_inf_principal_compl Finset.finite_toSet iInf_le_of_le Finset.coe_empty SetRel.preimage_empty_right Set.compl_empty principal_univ inf_of_le_left instReflLe mem_prod_same_iff NeBot.nonempty_of_mem Finset.coe_singleton iInf_le inf_le_right inter_mem
totallyBounded_iff_ultrafilter 📖	mathematical	—	TotallyBounded Cauchy Ultrafilter.toFilter	—	Ultrafilter.cauchy_of_totallyBounded' TotallyBounded.mono totallyBounded_iff_filter Ultrafilter.of_le LE.le.trans
totallyBounded_principal_iff 📖	mathematical	—	TotallyBounded principal TotallyBounded	—	SetRel.preimage_eq_biUnion
totallyBounded_sup 📖	mathematical	—	TotallyBounded Filter instSup	—	sup_eq_iSup totallyBounded_iSup Bool.instFinite

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchySeq_iff 📖	mathematical	Filter.HasBasis uniformity	CauchySeq PartialOrder.toPreorder SemilatticeSup.toPartialOrder SetRel Set.instMembership	—	cauchySeq_iff_tendsto Filter.prod_atTop_atTop_eq tendsto_iff prod_self Filter.atTop_basis SemilatticeSup.instIsDirectedOrder
cauchySeq_iff' 📖	mathematical	Filter.HasBasis uniformity	CauchySeq PartialOrder.toPreorder SemilatticeSup.toPartialOrder SetRel Set.instMembership	—	cauchySeq_iff le_rfl comp_symm_of_uniformity mem_of_mem mem_iff
cauchy_iff 📖	mathematical	Filter.HasBasis uniformity	Cauchy Filter.NeBot Set Filter Filter.instMembership SetRel Set.instMembership	—	le_basis_iff prod_self Filter.basis_sets
filter_totallyBounded_iff 📖	mathematical	Filter.HasBasis uniformity	Filter.TotallyBounded Set Set.Finite Filter Filter.instMembership SetRel.preimage	—	forall_iff Filter.mem_of_superset SetRel.preimage_subset_preimage_left
totallyBounded_iff 📖	mathematical	Filter.HasBasis uniformity	TotallyBounded Set Set.Finite Set.instHasSubset Set.iUnion Set.instMembership setOf SetRel	—	forall_iff HasSubset.Subset.trans Set.instIsTransSubset Set.iUnion₂_mono

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchySeq 📖	mathematical	Filter.Tendsto Filter.atTop PartialOrder.toPreorder SemilatticeSup.toPartialOrder nhds UniformSpace.toTopologicalSpace	CauchySeq PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	cauchy_map Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder
cauchy_map 📖	mathematical	Filter.Tendsto nhds UniformSpace.toTopologicalSpace	Cauchy Filter.map	—	Cauchy.mono Filter.map_neBot cauchy_nhds
subseq_mem_entourage 📖	mathematical	SetRel Filter Filter.instMembership uniformity Filter.Tendsto Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace	StrictMono Nat.instPreorder SetRel Set.instMembership	—	Filter.mem_atTop_sets SemilatticeSup.instIsDirectedOrder UniformSpace.ball_mem_nhds symm_le_uniformity CauchySeq.subseq_mem cauchySeq comp Filter.tendsto_add_atTop_nat StrictMono.add_const IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add le_add_self Nat.instCanonicallyOrderedAdd

Filter.TotallyBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_clusterPt 📖	mathematical	Filter.TotallyBounded	ClusterPt UniformSpace.toTopologicalSpace	—	Ultrafilter.of_le Ultrafilter.cauchy_of_totallyBounded' mono CompleteSpace.complete ClusterPt.mono le_nhds_iff_adhp_of_cauchy
exists_subset_of_mem 📖	mathematical	Filter.TotallyBounded Set Filter Filter.instMembership SetRel uniformity	Set Set.instHasSubset Set.Finite Filter Filter.instMembership SetRel.preimage	—	comp_symm_of_uniformity Set.range_subset_iff Set.finite_range Finite.of_fintype Set.Finite.inter_of_left Filter.mp_mem Filter.univ_mem' Subtype.coe_prop
isCompact_setOf_clusterPt 📖	mathematical	Filter.TotallyBounded	IsCompact UniformSpace.toTopologicalSpace setOf ClusterPt	—	TotallyBounded.isCompact_of_isClosed totallyBounded_setOf_clusterPt isClosed_setOf_clusterPt
map 📖	mathematical	Filter.TotallyBounded UniformContinuous	Filter.TotallyBounded Filter.map	—	Set.Finite.image
mono 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Filter.TotallyBounded	Filter.TotallyBounded	—	—
sup 📖	mathematical	Filter.TotallyBounded	Filter.TotallyBounded Filter Filter.instSup	—	Filter.totallyBounded_sup
totallyBounded_setOf_clusterPt 📖	mathematical	Filter.TotallyBounded	TotallyBounded setOf ClusterPt UniformSpace.toTopologicalSpace	—	Filter.HasBasis.totallyBounded_iff uniformity_hasBasis_closed SetRel.preimage_eq_biUnion IsClosed.closure_eq IsClosed.relPreimage_of_finite ClusterPt.mem_closure_of_mem

Function.Bijective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchySeq_comp_iff 📖	mathematical	Function.Bijective	CauchySeq Nat.instPreorder	—	CanLift.prf Equiv.instCanLiftForallCoeBijective Equiv.apply_symm_apply CauchySeq.comp_injective Nat.instNoMaxOrder Equiv.injective injective

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isComplete 📖	mathematical	—	IsComplete	—	CompleteSpace.complete isClosed_iff_clusterPt Filter.NeBot.mono le_inf

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isComplete 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace	IsComplete	—	isCompact_iff_totallyBounded_isComplete
totallyBounded 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace	TotallyBounded	—	isCompact_iff_totallyBounded_isComplete

IsComplete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
union 📖	mathematical	IsComplete	IsComplete Set Set.instUnion	—	—

SequentiallyComplete

Definitions

Name	Category	Theorems
seq 📖	CompOp	3 math math: seq_is_cauchySeq, seq_mem, seq_pair_mem
setSeq 📖	CompOp	5 math math: setSeq_mono, seq_mem, setSeq_mem, setSeq_sub_aux, setSeq_prod_subset
setSeqAux 📖	CompOp	1 math math: setSeq_sub_aux

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_nhds_of_seq_tendsto_nhds 📖	mathematical	Cauchy SetRel Filter Filter.instMembership uniformity Set.instHasSubset Filter.Tendsto seq Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds UniformSpace.toTopologicalSpace	—	le_nhds_of_cauchy_adhp_aux Filter.tendsto_atTop' SemilatticeSup.instIsDirectedOrder mem_nhds_left setSeq_mem le_max_left Set.Subset.trans setSeq_prod_subset le_max_right seq_mem
seq_is_cauchySeq 📖	mathematical	Cauchy SetRel Filter Filter.instMembership uniformity Set.instHasSubset	CauchySeq Nat.instPreorder seq	—	cauchySeq_of_controlled seq_pair_mem
seq_mem 📖	mathematical	Cauchy SetRel Filter Filter.instMembership uniformity	Set Set.instMembership setSeq seq	—	Filter.NeBot.nonempty_of_mem setSeq_mem
seq_pair_mem 📖	mathematical	Cauchy SetRel Filter Filter.instMembership uniformity	SetRel Set.instMembership seq	—	setSeq_prod_subset seq_mem
setSeq_mem 📖	mathematical	Cauchy SetRel Filter Filter.instMembership uniformity	Set Filter Filter.instMembership setSeq	—	Filter.biInter_mem Set.finite_le_nat
setSeq_mono 📖	mathematical	Cauchy SetRel Filter Filter.instMembership uniformity	Set Set.instHasSubset setSeq	—	Set.biInter_subset_biInter_left Set.Iic_subset_Iic
setSeq_prod_subset 📖	mathematical	Cauchy SetRel Filter Filter.instMembership uniformity	Set Set.instHasSubset SProd.sprod Set.instSProd setSeq	—	setSeq_sub_aux setSeq_mono
setSeq_sub_aux 📖	mathematical	Cauchy SetRel Filter Filter.instMembership uniformity	Set Set.instHasSubset setSeq Filter Filter.instMembership SProd.sprod Set.instSProd setSeqAux	—	Set.biInter_subset_of_mem Set.self_mem_Iic

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
totallyBounded 📖	mathematical	—	TotallyBounded	—	Set.mem_biUnion refl_mem_uniformity

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
totallyBounded 📖	mathematical	Set.Subsingleton	TotallyBounded	—	Set.Finite.totallyBounded finite

TotallyBounded

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure 📖	mathematical	TotallyBounded	TotallyBounded closure UniformSpace.toTopologicalSpace	—	closure_eq_cluster_pts Filter.TotallyBounded.totallyBounded_setOf_clusterPt Filter.totallyBounded_principal_iff
exists_subset 📖	mathematical	TotallyBounded SetRel Filter Filter.instMembership uniformity	Set Set.instHasSubset Set.Finite Set.iUnion Set.instMembership setOf SetRel	—	Filter.TotallyBounded.exists_subset_of_mem Filter.totallyBounded_principal_iff Filter.mem_principal_self
image 📖	mathematical	TotallyBounded UniformContinuous	TotallyBounded Set.image	—	Filter.TotallyBounded.map
insert 📖	mathematical	TotallyBounded	TotallyBounded Set Set.instInsert	—	totallyBounded_insert
isCompact_of_isClosed 📖	mathematical	TotallyBounded	IsCompact UniformSpace.toTopologicalSpace	—	isCompact_of_isComplete IsClosed.isComplete
isCompact_of_isComplete 📖	mathematical	TotallyBounded IsComplete	IsCompact UniformSpace.toTopologicalSpace	—	isCompact_iff_totallyBounded_isComplete
isSeparable 📖	mathematical	TotallyBounded	TopologicalSpace.IsSeparable UniformSpace.toTopologicalSpace	—	UniformSpace.subset_countable_closure_of_almost_dense_set Filter.mem_of_superset symmetrize_mem_uniformity SetRel.symmetrize_subset_inv Set.Finite.countable
subset 📖	mathematical	Set Set.instHasSubset TotallyBounded	TotallyBounded	—	Set.Subset.trans
union 📖	mathematical	TotallyBounded	TotallyBounded Set Set.instUnion	—	totallyBounded_union

Ultrafilter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchy_of_totallyBounded 📖	mathematical	TotallyBounded Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder toFilter Filter.principal	Cauchy toFilter	—	cauchy_of_totallyBounded' Filter.TotallyBounded.mono Filter.totallyBounded_principal_iff
cauchy_of_totallyBounded' 📖	mathematical	Filter.TotallyBounded toFilter	Cauchy toFilter	—	neBot' comp_symm_of_uniformity eventually_exists_mem_iff Filter.mem_of_superset Filter.prod_mem_prod Set.Subset.trans

UniformContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_cauchySeq 📖	mathematical	UniformContinuous CauchySeq	CauchySeq	—	Cauchy.map

UniformSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
complete_of_cauchySeq_tendsto 📖	mathematical	Filter.Tendsto Filter.atTop Nat.instPreorder nhds toTopologicalSpace	CompleteSpace	—	Filter.exists_antitone_seq complete_of_convergent_controlled_sequences Set.Subset.refl cauchySeq_of_controlled
complete_of_convergent_controlled_sequences 📖	mathematical	SetRel Filter Filter.instMembership uniformity Filter.Tendsto Filter.atTop Nat.instPreorder nhds toTopologicalSpace	CompleteSpace	—	Filter.exists_antitone_seq Filter.inter_mem Set.Subset.refl SequentiallyComplete.le_nhds_of_seq_tendsto_nhds Set.Subset.trans Set.inter_subset_right Set.inter_subset_left SequentiallyComplete.seq_pair_mem
firstCountableTopology 📖	mathematical	—	FirstCountableTopology toTopologicalSpace	—	nhds_eq_comap_uniformity Filter.comap.isCountablyGenerated
secondCountable_of_almost_dense_set 📖	mathematical	Set Set.Countable Set.iUnion Set.instMembership ball Set.univ	SecondCountableTopology toTopologicalSpace	—	subset_countable_closure_of_almost_dense_set Set.mem_univ secondCountable_of_separable
secondCountable_of_separable 📖	mathematical	—	SecondCountableTopology toTopologicalSpace	—	TopologicalSpace.exists_countable_dense Filter.HasBasis.exists_antitone_subbasis uniformity_hasBasis_open_symmetric Set.Countable.biUnion Set.countable_range instCountableNat TopologicalSpace.IsTopologicalBasis.eq_generateFrom TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds isOpen_ball mem_nhds_iff IsOpen.mem_nhds comp_symm_of_uniformity Filter.HasBasis.mem_iff Filter.HasAntitoneBasis.toHasBasis Dense.inter_open_nonempty mem_ball_self SetRel.symm ball_subset_of_comp_subset
subset_countable_closure_of_almost_dense_set 📖	mathematical	Set Set.Countable Set.instHasSubset Set.iUnion Set.instMembership ball	Set Set.instHasSubset Set.Countable closure toTopologicalSpace	—	has_seq_basis Filter.HasAntitoneBasis.mem Set.Countable.to_subtype Set.iUnion₂_subset Set.range_subset_iff Set.countable_iUnion instCountableNat Set.countable_range Prop.countable mem_closure_iff_ball comp_mem_uniformity_sets Filter.HasAntitoneBasis.mem_iff Set.mem_iUnion₂ ball_mono HasSubset.Subset.trans Set.instIsTransSubset SetRel.comp_subset_comp mem_ball_comp mem_ball_symmetry Set.mem_iUnion₂_of_mem Set.mem_range_self

(root)

Definitions

Name	Category	Theorems
Cauchy 📖	MathDef	57 math math: cauchy_pi_iff', IsUniformAddGroup.cauchy_map_iff_tendsto, UniformCauchySeqOn.cauchy_map, Filter.totallyBounded_iff_filter, cauchy_inf_uniformSpace, cauchy_iff, cauchy_map_iff_exists_tendsto, Cauchy.comap', Cauchy.map, cauchy_iInf_uniformSpace', cauchy_map_iff, cauchy_iff_exists_le_nhds, CauchyFilter.cauchyFilter_eq, cauchy_comap_uniformSpace, Cauchy.mono, BoxIntegral.Integrable.cauchy_map_integralSum_toFilteriUnion, cauchy_map_of_uniformCauchySeqOn_fderiv, CauchyFilter.inseparable_iff, Cauchy.ultrafilter_of, CauchyFilter.instNeBotValFilterCauchy, Valuation.cauchy_iff, cauchy_prod_iff, IsUniformAddGroup.cauchy_iff_tendsto_swapped, Valued.cauchy_iff, IsUniformGroup.cauchy_map_iff_tendsto, Cauchy.prod, Metric.cauchy_iff, Cauchy.map_of_le, IsUniformAddGroup.cauchy_iff_tendsto, IsUniformGroup.cauchy_iff_tendsto_swapped, Cauchy.pi, EMetric.cauchy_iff, Filter.totallyBounded_iff_ultrafilter, BoxIntegral.integrable_iff_cauchy, Filter.HasBasis.cauchy_iff, Ultrafilter.cauchy_of_totallyBounded, cauchy_pure, cauchy_iff_le, cauchy_map_iff', cauchy_pi_iff, Cauchy.mono_uniformSpace, IsUniformAddGroup.cauchy_map_iff_tendsto_swapped, Ultrafilter.cauchy_of_totallyBounded', totallyBounded_iff_filter, Cauchy.comap, CauchyFilter.inseparable_lim_iff, totallyBounded_iff_ultrafilter, IsUniformGroup.cauchy_iff_tendsto, cauchy_nhds, IsUniformGroup.cauchy_map_iff_tendsto_swapped, cauchy_iInf_uniformSpace, AddGroupFilterBasis.cauchy_iff, Cauchy.mono', IsUniformInducing.cauchy_map_iff, Filter.Tendsto.cauchy_map, cauchy_iff', CompletableTopField.nice
CauchySeq 📖	MathDef	79 math math: UniformCauchySeqOn.cauchySeq, Metric.cauchySeq_iff, NormedAddCommGroup.cauchy_series_of_le_geometric'', NormedCommGroup.cauchySeq_iff, MeasureTheory.Lp.cauchySeq_Lp_iff_cauchySeq_eLpNorm, NormedAddCommGroup.cauchy_series_of_le_geometric', cauchySeq_iff', cauchySeq_finset_iff_nat_tsum_vanishing, cauchySeq_iff_tendsto_dist_atTop_0, cauchySeq_of_edist_le_of_tsum_ne_top, Filter.HasBasis.cauchySeq_iff, cauchySeq_of_le_geometric, cauchySeq_finset_of_summable_norm, CauchySeq.mul_const, cauchySeq_finset_iff_nat_tprod_vanishing, SequentiallyComplete.seq_is_cauchySeq, cauchySeq_range_of_norm_bounded, cauchySeq_finset_of_norm_bounded_eventually, CauchySeq.prodMap, CauchySeq.mul, cauchySeq_of_edist_le_of_summable, EMetric.cauchySeq_iff, cauchySeq_finset_iff_vanishing_norm, cauchySeq_of_edist_le_geometric_two, NormedAddCommGroup.cauchySeq_iff, Filter.HasBasis.cauchySeq_iff', SeminormedAddCommGroup.cauchySeq_of_le_geometric, Monotone.cauchySeq_series_mul_of_tendsto_zero_of_bounded, CauchySeq.comp_injective, CauchySeq.const_mul, Filter.Tendsto.cauchySeq, CauchySeq.add_const, multipliable_iff_cauchySeq_finset, cauchySeq_of_dist_le_of_summable, CauchySeq.add, LipschitzOnWith.cauchySeq_comp, cauchySeq_of_le_tendsto_0, cauchySeq_finset_iff_prod_vanishing, Antitone.cauchySeq_series_mul_of_tendsto_zero_of_bounded, cauchySeq_finset_iff_tprod_vanishing, cauchySeq_const, NonarchimedeanGroup.cauchySeq_of_tendsto_div_nhds_one, CauSeq.cauchySeq, cauchySeq_iff_le_tendsto_0, EMetric.cauchySeq_iff_le_tendsto_0, Function.Bijective.cauchySeq_comp_iff, cauchySeq_of_edist_le_geometric, isCauSeq_iff_cauchySeq, CauchySeq.prodMk, CauchySeq.inv, NonarchimedeanAddGroup.cauchySeq_of_tendsto_sub_nhds_zero, cauchySeq_finset_of_norm_bounded, summable_iff_cauchySeq_finset, cauchySeq_finset_iff_sum_vanishing, summable_iff_cauchySeq_finset_and_tsum_mem, EMetric.cauchySeq_iff_NNReal, cauchySeq_of_summable_dist, CauchySeq.comp_tendsto, cauchySeq_shift, Antitone.cauchySeq_alternating_series_of_tendsto_zero, CauchySeq.neg, cauchySeq_iff_tendsto, cauchySeq_of_le_geometric_two, EMetric.cauchySeq_iff', Monotone.cauchySeq_alternating_series_of_tendsto_zero, cauchy_series_of_le_geometric, Metric.cauchySeq_iff', LipschitzWith.cauchySeq_comp, cauchySeq_prod_of_eventually_eq, UniformContinuous.comp_cauchySeq, cauchySeq_of_controlled, NonarchimedeanAddGroup.cauchySeq_sum_of_tendsto_cofinite_zero, cauchySeq_iff, cauchySeq_finset_iff_tsum_vanishing, cauchySeq_finset_of_geometric_bound, cauchySeq_of_le_tendsto_0', CauchySeq.const_add, NonarchimedeanGroup.cauchySeq_prod_of_tendsto_cofinite_one, cauchySeq_sum_of_eventually_eq
CompleteSpace 📖	CompData	150 math math: TrivSqZeroExt.instCompleteSpace, complete_of_proper, QuotientAddGroup.completeSpace_right', PiLp.completeSpace, TopologicalSpace.Compacts.completeSpace_iff, IsComplete.completeSpace_coe, DiscreteUniformity.instCompleteSpace, ContinuousLinearMap.completeSpace_eqLocus, Valued.integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField, WithLp.instCompleteSpace, CompleteSpace.mulOpposite, TopologicalSpace.IsCompletelyPseudoMetrizableSpace.complete, completeSpace_iff_ultrafilter, QuotientGroup.completeSpace_left, NormedAddCommGroup.summable_imp_tendsto_iff_completeSpace, completeSpace_extension, QuotientAddGroup.completeSpace_left, completeSpace_congr, TopologicalSpace.Opens.CompleteCopy.instCompleteSpace, ContinuousLinearMap.completeSpace, Matrix.instCompleteSpace, CompleteSpace.addOpposite, IsAdic.isPrecomplete_iff, QuotientGroup.completeSpace_right, SeparatingDual.completeSpace_of_completeSpace_continuousMultilinearMap, Algebra.elemental.instCompleteSpaceSubtypeMemSubalgebra, Submodule.Quotient.completeSpace, IsAdic.isAdicComplete_iff, QuotientAddGroup.completeSpace_right, ContinuousMapZero.instCompleteSpaceOfT1SpaceOfContinuousMap, QuotientGroup.completeSpace_right', UniformFun.instCompleteSpace, IsometryEquiv.completeSpace, MeasureTheory.Lp.instCompleteSpace, CStarAlgebra.toCompleteSpace, ContinuousMultilinearMap.completeSpace, completeSpace_iff_isComplete_univ, spectralNorm.completeSpace, SeparationQuotient.completeSpace_iff, IsTopologicalGroup.completeSpace_rightUniformSpace_iff_leftUniformSpace, Quaternion.instCompleteSpaceReal, UniformOnFun.instCompleteSpace, WithCStarModule.instCompleteSpace, TopologicalSpace.NonemptyCompacts.completeSpace_iff, Padic.instCompleteSpace, Metric.complete_of_convergent_controlled_sequences, CompletePseudometrizable.iInf, IsometryEquiv.completeSpace_iff, CStarMatrix.instCompleteSpace, completeSpace_of_isComplete_univ, TopologicalSpace.complete_completelyPseudoMetrizableMetric, TopologicalSpace.UpgradedIsCompletelyMetrizableSpace.toCompleteSpace, PadicInt.completeSpace, WithLp.instProdCompleteSpace, ContinuousLinearMap.instCompleteSpace, IsRightUniformGroup.completeSpace_of_weaklyLocallyCompactSpace, IsUniformInducing.completeSpace, RCLike.toCompleteSpace, LinearIsometryEquiv.completeSpace_map, NonUnitalCommCStarAlgebra.toCompleteSpace, PiNat.completeSpace, CompleteSpace.prod, ContinuousMultilinearMap.instCompleteSpace, UniformSpace.Completion.completeSpace, ContinuousMap.instCompleteSpaceOfCompactlyCoherentSpace, UniformEquiv.completeSpace_iff, MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpSubmoduleLpMeasOfFactLeMeasurableSpace, ZeroAtInftyContinuousMap.instCompleteSpace, NonUnitalAlgebra.elemental.instCompleteSpaceSubtypeMemNonUnitalSubalgebra, StarAlgebra.elemental.instCompleteSpaceSubtypeMemStarSubalgebra, Complex.instCompleteSpace, TopologicalSpace.Closeds.instCompleteSpace, Valued.integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField, GromovHausdorff.instCompleteSpaceGHSpace, SeparatingDual.completeSpace_continuousLinearMap_iff, completeSpace_prod_of_nonempty, UniformConvergenceCLM.completeSpace, ContinuousAlternatingMap.completeSpace, CompleteSpace.iInf, Metric.complete_of_cauchySeq_tendsto, CauchyFilter.instCompleteSpace, UniformSpace.complete_of_cauchySeq_tendsto, QuotientGroup.completeSpace_left', CpltSepUniformSpace.completeSpace, Tactic.ComputeAsymptotics.Seq.instCompleteSpaceStream', SeparatingDual.completeSpace_of_completeSpace_continuousLinearMap, Tactic.ComputeAsymptotics.Seq.instCompleteSpaceSeq, WStarAlgebra.exists_predual, TopologicalSpace.complete_completelyMetrizableMetric, IsTopologicalAddGroup.completeSpace_rightUniformSpace_iff_leftUniformSpace, NormedField.completeSpace_iff_isComplete_closedBall, Real.instCompleteSpace, MeasureTheory.Lp.completeSpace_lp_of_cauchy_complete_eLpNorm, completeSpace_of_cauSeq_isComplete, ArithmeticFunction.instCompleteSpace, Metric.Sigma.completeSpace, TopologicalSpace.NonemptyCompacts.instCompleteSpace, LinearIsometry.completeSpace_map, LaurentSeries.instLaurentSeriesComplete, UniformSpace.complete_of_convergent_controlled_sequences, instCompleteSpaceSubtypeMemSubmoduleOfIsClosedCoe, Pi.complete, ContinuousAlternatingMap.instCompleteSpace, EMetric.complete_of_convergent_controlled_sequences, CpltSepUniformSpace.isCompleteSpace, NonUnitalCStarAlgebra.toCompleteSpace, ODE.FunSpace.instCompleteSpace, TopologicalSpace.Compacts.instCompleteSpace, SeparationQuotient.instCompleteSpace, ContinuousLinearMap.completeSpace_ker, Path.instCompleteSpace, TopologicalSpace.IsCompletelyMetrizableSpace.complete, CompleteSpace.fst_of_prod, NormedAddCommGroup.completeSpace_of_summable_imp_tendsto, SeparatingDual.completeSpace_continuousMultilinearMap_iff, Submodule.instOrthogonalCompleteSpace, MeasureTheory.integral_def, AntilipschitzWith.completeSpace_range_clm, CompleteSpace.sum, EMetric.complete_of_cauchySeq_tendsto, lp.completeSpace, IsNonarchimedeanLocalField.instCompleteSpace, ContinuousAlgHom.instCompleteSpaceSubtypeMemSubalgebraEqualizerOfT2SpaceOfContinuousMapClass, IsClosed.completeSpace_coe, Unitization.instCompleteSpace, ULift.instCompleteSpace, BoundedContinuousFunction.instCompleteSpace, MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpLpMeasSubgroupOfFactLeMeasurableSpace, MvPowerSeries.WithPiTopology.instCompleteSpace, FiniteDimensional.complete, completeSpace_coe_iff_isComplete, completeSpace_iff_isComplete_range, IsRightUniformAddGroup.completeSpace_of_weaklyLocallyCompactSpace, IsNonarchimedeanLocalField.instCompleteSpaceSubtypeMemSubringIntegerValueGroupWithZeroValuation, complete_of_compact, NonUnitalStarAlgebra.elemental.instCompleteSpaceSubtypeMemNonUnitalStarSubalgebra, instCompleteSpaceSubtypeMemClosedSubmodule, AbstractCompletion.complete, DoubleCentralizer.instCompleteSpace, CommCStarAlgebra.toCompleteSpace, IsUniformInducing.completeSpace_congr, TopologicalSpace.UpgradedIsCompletelyPseudoMetrizableSpace.toCompleteSpace, Submodule.topologicalClosure.completeSpace, StarSubalgebra.instCompleteSpaceSubtypeMemTopologicalClosure, QuotientAddGroup.completeSpace_left', completeSpace_ulift_iff, PowerSeries.WithPiTopology.instCompleteSpace, CompleteSpace.snd_of_prod, NNReal.instCompleteSpace, SemiNormedGrp.completion_completeSpace
IsComplete 📖	MathDef	30 math math: complete_univ, LinearIsometry.isComplete_image_iff', ContinuousLinearMap.isComplete_ker, IsSeqCompact.isComplete, isComplete_iff_ultrafilter, LinearIsometry.isComplete_map_iff, completeSpace_iff_isComplete_univ, LinearIsometry.isComplete_image_iff, IsComplete.union, isComplete_of_complete_image, IsUniformEmbedding.isComplete_iff, Submodule.complete_of_finiteDimensional, IsUniformInducing.isComplete_range, isCompact_iff_totallyBounded_isComplete, Subtype.isComplete_iff, IsUniformInducing.isComplete_iff, NormedField.completeSpace_iff_isComplete_closedBall, isComplete_iff_clusterPt, isComplete_iUnion_separated, MeasureTheory.isComplete_aestronglyMeasurable, IsClosed.isComplete, IsCompact.isComplete, AntilipschitzWith.isComplete_range, ContinuousMap.isComplete_setOf_eqOn, isComplete_image_iff, LinearIsometry.isComplete_map_iff', completeSpace_coe_iff_isComplete, completeSpace_iff_isComplete_range, QuasiCompleteSpace.quasiComplete, isComplete_iff_ultrafilter'
interUnionBalls 📖	CompOp	2 math math: isCompact_closure_interUnionBalls, totallyBounded_interUnionBalls

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cauchySeq_const 📖	mathematical	—	CauchySeq PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	Filter.Tendsto.cauchySeq tendsto_const_nhds
cauchySeq_iff 📖	mathematical	—	CauchySeq Nat.instPreorder Set Set.instMembership	—	SemilatticeSup.instIsDirectedOrder
cauchySeq_iff' 📖	mathematical	—	CauchySeq Nat.instPreorder Filter.Eventually Set Set.instMembership Set.preimage Filter.atTop Prod.instPreorder	—	cauchySeq_iff_tendsto
cauchySeq_iff_tendsto 📖	mathematical	—	CauchySeq PartialOrder.toPreorder SemilatticeSup.toPartialOrder Filter.Tendsto Filter.atTop Prod.instPreorder uniformity	—	cauchy_map_iff' Filter.atTop_neBot SemilatticeSup.instIsDirectedOrder Filter.prod_atTop_atTop_eq Prod.map_def
cauchySeq_of_controlled 📖	mathematical	SetRel Set.instHasSubset Set.instMembership	CauchySeq PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	cauchySeq_iff_tendsto Filter.mem_map Filter.mem_atTop_sets SemilatticeSup.instIsDirectedOrder
cauchySeq_shift 📖	mathematical	—	CauchySeq Nat.instPreorder	—	cauchySeq_iff CauchySeq.comp_tendsto Filter.tendsto_add_atTop_nat
cauchySeq_tendsto_of_complete 📖	mathematical	CauchySeq	Filter.Tendsto Filter.atTop nhds UniformSpace.toTopologicalSpace	—	CompleteSpace.complete
cauchySeq_tendsto_of_isComplete 📖	mathematical	IsComplete Set Set.instMembership CauchySeq	Set Set.instMembership Filter.Tendsto Filter.atTop nhds UniformSpace.toTopologicalSpace	—	Filter.le_principal_iff Filter.mem_map_iff_exists_image Filter.univ_mem Set.image_univ Set.range_subset_iff
cauchy_comap_uniformSpace 📖	mathematical	—	Cauchy UniformSpace.comap Filter.map	—	Filter.prod_map_map_eq
cauchy_iInf_uniformSpace 📖	mathematical	—	Cauchy iInf UniformSpace instInfSetUniformSpace	—	iInf_uniformity le_iInf_iff
cauchy_iInf_uniformSpace' 📖	mathematical	—	Cauchy iInf UniformSpace instInfSetUniformSpace	—	cauchy_iff_le iInf_uniformity
cauchy_iff 📖	mathematical	—	Cauchy Filter.NeBot Set Filter Filter.instMembership Set.instHasSubset SProd.sprod Set.instSProd	—	cauchy_iff'
cauchy_iff' 📖	mathematical	—	Cauchy Filter.NeBot Set Filter Filter.instMembership Set.instMembership	—	Filter.HasBasis.cauchy_iff Filter.basis_sets
cauchy_iff_exists_le_nhds 📖	mathematical	—	Cauchy Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds UniformSpace.toTopologicalSpace	—	CompleteSpace.complete Cauchy.mono cauchy_nhds
cauchy_iff_le 📖	mathematical	—	Cauchy Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder SProd.sprod Filter.instSProd uniformity	—	—
cauchy_inf_uniformSpace 📖	mathematical	—	Cauchy UniformSpace instMinUniformSpace	—	inf_uniformity le_inf_iff
cauchy_map_iff 📖	mathematical	—	Cauchy Filter.map Filter.NeBot Filter.Tendsto SProd.sprod Filter Filter.instSProd uniformity	—	Cauchy.eq_1 Filter.map_neBot_iff Filter.prod_map_map_eq Filter.Tendsto.eq_1
cauchy_map_iff' 📖	mathematical	—	Cauchy Filter.map Filter.Tendsto SProd.sprod Filter Filter.instSProd uniformity	—	cauchy_map_iff
cauchy_map_iff_exists_tendsto 📖	mathematical	—	Cauchy Filter.map Filter.Tendsto nhds UniformSpace.toTopologicalSpace	—	cauchy_iff_exists_le_nhds Filter.map_neBot
cauchy_nhds 📖	mathematical	—	Cauchy nhds UniformSpace.toTopologicalSpace	—	nhds_neBot Eq.trans_le nhds_prod_eq nhds_le_uniformity
cauchy_prod_iff 📖	mathematical	—	Cauchy instUniformSpaceProd Filter.map	—	—
cauchy_pure 📖	mathematical	—	Cauchy Filter Filter.instPure	—	Cauchy.mono Filter.pure_neBot cauchy_nhds pure_le_nhds
completeSpace_iff_isComplete_univ 📖	mathematical	—	CompleteSpace IsComplete Set.univ	—	complete_univ completeSpace_of_isComplete_univ
completeSpace_iff_ultrafilter 📖	mathematical	—	CompleteSpace Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Ultrafilter.toFilter nhds UniformSpace.toTopologicalSpace	—	Filter.principal_univ
completeSpace_of_isComplete_univ 📖	mathematical	IsComplete Set.univ	CompleteSpace	—	le_top Filter.principal_univ
completeSpace_prod_of_nonempty 📖	mathematical	—	CompleteSpace instUniformSpaceProd	—	CompleteSpace.fst_of_prod CompleteSpace.snd_of_prod CompleteSpace.prod
complete_of_compact 📖	mathematical	—	CompleteSpace	—	Filter.principal_univ isCompact_iff_totallyBounded_isComplete isCompact_univ
complete_univ 📖	mathematical	—	IsComplete Set.univ	—	CompleteSpace.complete Set.mem_univ
isCompact_closure_interUnionBalls 📖	mathematical	Filter.HasBasis uniformity	IsCompact UniformSpace.toTopologicalSpace closure interUnionBalls	—	isCompact_iff_totallyBounded_isComplete TotallyBounded.closure totallyBounded_interUnionBalls IsClosed.isComplete isClosed_closure
isCompact_iff_totallyBounded_isComplete 📖	mathematical	—	IsCompact UniformSpace.toTopologicalSpace TotallyBounded IsComplete	—	totallyBounded_iff_ultrafilter isCompact_iff_ultrafilter_le_nhds Cauchy.mono Ultrafilter.neBot cauchy_nhds le_nhds_of_cauchy_adhp
isComplete_iUnion_separated 📖	mathematical	IsComplete SetRel Filter Filter.instMembership uniformity	IsComplete Set.iUnion	—	cauchy_iff Set.inter_subset_right Filter.inter_mem Filter.le_principal_iff Set.Subset.trans Set.prod_mono Set.inter_subset_left Filter.nonempty_of_mem Set.mem_iUnion Set.mk_mem_prod Filter.mem_of_superset
isComplete_iff_clusterPt 📖	mathematical	—	IsComplete Set Set.instMembership ClusterPt UniformSpace.toTopologicalSpace	—	le_nhds_iff_adhp_of_cauchy
isComplete_iff_ultrafilter 📖	mathematical	—	IsComplete Set Set.instMembership Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Ultrafilter.toFilter nhds UniformSpace.toTopologicalSpace	—	isComplete_iff_clusterPt Cauchy.ultrafilter_of LE.le.trans Ultrafilter.of_le ClusterPt.mono ClusterPt.of_le_nhds Ultrafilter.neBot
isComplete_iff_ultrafilter' 📖	mathematical	—	IsComplete Set Set.instMembership Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Ultrafilter.toFilter nhds UniformSpace.toTopologicalSpace	—	isComplete_iff_ultrafilter
le_nhds_iff_adhp_of_cauchy 📖	mathematical	Cauchy	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds UniformSpace.toTopologicalSpace ClusterPt	—	ClusterPt.of_le_nhds' le_nhds_of_cauchy_adhp
le_nhds_of_cauchy_adhp 📖	mathematical	Cauchy	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds UniformSpace.toTopologicalSpace	—	le_nhds_of_cauchy_adhp_aux cauchy_iff Filter.forall_mem_nonempty_iff_neBot Filter.inter_mem_inf mem_nhds_left
le_nhds_of_cauchy_adhp_aux 📖	mathematical	Set Filter Filter.instMembership Set.instHasSubset SProd.sprod Set.instSProd Set.instMembership	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds UniformSpace.toTopologicalSpace	—	comp_mem_uniformity_sets mem_nhds_uniformity_iff_right Filter.mem_of_superset SetRel.prodMk_mem_comp Set.mk_mem_prod
tendsto_nhds_of_cauchySeq_of_subseq 📖	mathematical	CauchySeq Filter.Tendsto Filter.atTop nhds UniformSpace.toTopologicalSpace	Filter.Tendsto Filter.atTop nhds UniformSpace.toTopologicalSpace	—	le_nhds_of_cauchy_adhp MapClusterPt.of_comp Filter.Tendsto.mapClusterPt
totallyBounded_biUnion 📖	mathematical	—	TotallyBounded Set.iUnion Set Set.instMembership	—	Set.Finite.to_subtype Set.biUnion_eq_iUnion totallyBounded_iUnion
totallyBounded_closure 📖	mathematical	—	TotallyBounded closure UniformSpace.toTopologicalSpace	—	TotallyBounded.subset subset_closure TotallyBounded.closure
totallyBounded_empty 📖	mathematical	—	TotallyBounded Set Set.instEmptyCollection	—	Set.Finite.totallyBounded Set.finite_empty
totallyBounded_iUnion 📖	mathematical	—	TotallyBounded Set.iUnion	—	—
totallyBounded_iff_filter 📖	mathematical	—	TotallyBounded Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder Cauchy	—	Filter.totallyBounded_principal_iff Filter.totallyBounded_iff_filter
totallyBounded_iff_subset 📖	mathematical	—	TotallyBounded Set Set.instHasSubset Set.Finite Set.iUnion Set.instMembership setOf	—	TotallyBounded.exists_subset
totallyBounded_iff_ultrafilter 📖	mathematical	—	TotallyBounded Cauchy Ultrafilter.toFilter	—	Filter.totallyBounded_principal_iff Filter.totallyBounded_iff_ultrafilter
totallyBounded_insert 📖	mathematical	—	TotallyBounded Set Set.instInsert	—	—
totallyBounded_interUnionBalls 📖	mathematical	Filter.HasBasis uniformity	TotallyBounded interUnionBalls	—	Filter.HasBasis.totallyBounded_iff Set.mem_iInter Finset.finite_toSet Set.iUnion_congr_Prop Finset.coe_image Finset.coe_range Set.iUnion_exists Set.biUnion_and' Set.iUnion_iUnion_eq_right
totallyBounded_of_forall_isSymm 📖	mathematical	Set Set.Finite Set.instHasSubset Set.iUnion Set.instMembership UniformSpace.ball	TotallyBounded	—	Filter.HasBasis.totallyBounded_iff UniformSpace.hasBasis_symmetric Set.iUnion_congr_Prop UniformSpace.ball_eq_of_symmetry
totallyBounded_sSup 📖	mathematical	—	Filter.TotallyBounded SupSet.sSup Filter Filter.instSupSet	—	sSup_eq_iSup Filter.totallyBounded_biSup
totallyBounded_sUnion 📖	mathematical	—	TotallyBounded Set.sUnion	—	Set.sUnion_eq_biUnion totallyBounded_biUnion
totallyBounded_singleton 📖	mathematical	—	TotallyBounded Set Set.instSingletonSet	—	Set.Finite.totallyBounded Set.finite_singleton
totallyBounded_union 📖	mathematical	—	TotallyBounded Set Set.instUnion	—	Set.union_eq_iUnion totallyBounded_iUnion Bool.instFinite

---

← Back to Index