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`, `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`, `isCompact_of_totallyBounded_isClosed`, `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` 📖	—	`Cauchy` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.comap` `uniformity`	—	—	`Filter.prod_comap_comap_eq` `Filter.comap_mono`
`comap'` 📖	—	`Cauchy` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.comap` `uniformity`	—	—	`comap`
`le_nhds_lim` 📖	mathematical	`Cauchy`	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `nhds` `UniformSpace.toTopologicalSpace` `lim` `Filter.NeBot.nonempty` `Filter.NeBot` `SProd.sprod` `Filter.instSProd` `uniformity`	—	`le_nhds_lim` `CompleteSpace.complete`
`map` 📖	mathematical	`Cauchy` `UniformContinuous`	`Filter.map`	—	`Filter.NeBot.map` `Filter.prod_map_map_eq` `Filter.map_mono`
`mono` 📖	—	`Cauchy` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	—	—	`le_trans` `Filter.prod_mono`
`mono'` 📖	—	`Cauchy` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	—	—	`mono`
`mono_uniformSpace` 📖	—	`UniformSpace` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderUniformSpace` `Cauchy`	—	—	`LE.le.trans`
`prod` 📖	mathematical	`Cauchy`	`instUniformSpaceProd` `SProd.sprod` `Filter` `Filter.instSProd`	—	`Filter.map_fst_prod` `Filter.map_snd_prod`
`ultrafilter_of` 📖	mathematical	`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`	`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` 📖	—	`CauchySeq` `Filter.Tendsto` `Filter.atTop` `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` `Set.instMembership` `Filter.atTop`	—	`Filter.eventually_atTop_curry` `tendsto_uniformity`
`mem_entourage` 📖	mathematical	`CauchySeq` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SetRel` `Filter` `Filter.instMembership` `uniformity`	`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`	`instUniformSpaceProd` `Prod.instPreorder`	—	`Filter.prod_map_map_eq'` `Filter.prod_atTop_atTop_eq` `Cauchy.prod`
`prodMk` 📖	mathematical	`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` `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` `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` `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` `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` `forall_swap`
`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.Finite` `Set` `Filter` `Filter.instMembership` `SetRel.preimage`	—	`forall_iff` `Filter.mem_of_superset` `SetRel.preimage_subset_preimage_left`
`totallyBounded_iff` 📖	mathematical	`Filter.HasBasis` `uniformity`	`TotallyBounded` `Set.Finite` `Set` `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`	—	`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` `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` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `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.instHasSubset` `Set.Finite` `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.map`	—	`Set.Finite.image`
`mono` 📖	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.TotallyBounded`	—	—	—
`sup` 📖	mathematical	`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`	`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`	`Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	—	`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`	`Set.instMembership` `seq`	—	`setSeq_prod_subset` `seq_mem`
`setSeq_mem` 📖	mathematical	`Cauchy` `SetRel` `Filter` `Filter.instMembership` `uniformity`	`Set` `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` `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`	`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`	—	`Filter.TotallyBounded.exists_subset_of_mem` `Filter.totallyBounded_principal_iff` `Filter.mem_principal_self`
`image` 📖	mathematical	`TotallyBounded` `UniformContinuous`	`Set.image`	—	`Filter.TotallyBounded.map`
`insert` 📖	mathematical	`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` 📖	—	`Set` `Set.instHasSubset` `TotallyBounded`	—	—	`Set.Subset.trans`
`union` 📖	mathematical	`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`	—	`cauchy_of_totallyBounded'` `Filter.TotallyBounded.mono` `Filter.totallyBounded_principal_iff`
`cauchy_of_totallyBounded'` 📖	mathematical	`Filter.TotallyBounded` `toFilter`	`Cauchy`	—	`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` 📖	—	`UniformContinuous` `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.Countable` `Set.iUnion` `Set` `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.Countable` `Set` `Set.instHasSubset` `Set.iUnion` `Set.instMembership` `ball`	`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	44 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_iInf_uniformSpace'`, `cauchy_map_iff`, `cauchy_iff_exists_le_nhds`, `CauchyFilter.cauchyFilter_eq`, `cauchy_comap_uniformSpace`, `BoxIntegral.Integrable.cauchy_map_integralSum_toFilteriUnion`, `CauchyFilter.inseparable_iff`, `CauchyFilter.instNeBotValFilterCauchy`, `cauchy_prod_iff`, `IsUniformAddGroup.cauchy_iff_tendsto_swapped`, `Valued.cauchy_iff`, `IsUniformGroup.cauchy_map_iff_tendsto`, `Metric.cauchy_iff`, `IsUniformAddGroup.cauchy_iff_tendsto`, `IsUniformGroup.cauchy_iff_tendsto_swapped`, `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`, `IsUniformAddGroup.cauchy_map_iff_tendsto_swapped`, `Ultrafilter.cauchy_of_totallyBounded'`, `totallyBounded_iff_filter`, `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`, `IsUniformInducing.cauchy_map_iff`, `Filter.Tendsto.cauchy_map`, `cauchy_iff'`
`CauchySeq` 📖	MathDef	61 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_finset_iff_nat_tprod_vanishing`, `SequentiallyComplete.seq_is_cauchySeq`, `cauchySeq_finset_of_norm_bounded_eventually`, `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`, `Filter.Tendsto.cauchySeq`, `multipliable_iff_cauchySeq_finset`, `cauchySeq_of_dist_le_of_summable`, `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`, `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_shift`, `Antitone.cauchySeq_alternating_series_of_tendsto_zero`, `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'`, `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'`, `NonarchimedeanGroup.cauchySeq_prod_of_tendsto_cofinite_one`
`CompleteSpace` 📖	CompData	139 math math: `TrivSqZeroExt.instCompleteSpace`, `complete_of_proper`, `QuotientAddGroup.completeSpace_right'`, `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`, `Padic.instCompleteSpace`, `Metric.complete_of_convergent_controlled_sequences`, `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`, `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`, `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`, `TopologicalSpace.NonemptyCompacts.instCompleteSpace`, `LinearIsometry.completeSpace_map`, `LaurentSeries.instLaurentSeriesComplete`, `UniformSpace.complete_of_convergent_controlled_sequences`, `instCompleteSpaceSubtypeMemSubmoduleOfIsClosedCoe`, `ContinuousAlternatingMap.instCompleteSpace`, `EMetric.complete_of_convergent_controlled_sequences`, `CpltSepUniformSpace.isCompleteSpace`, `NonUnitalCStarAlgebra.toCompleteSpace`, `ODE.FunSpace.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`, `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	27 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`, `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`, `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`	`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`
`isCompact_of_totallyBounded_isClosed` 📖	mathematical	`TotallyBounded`	`IsCompact` `UniformSpace.toTopologicalSpace`	—	`TotallyBounded.isCompact_of_isClosed`
`isComplete_iUnion_separated` 📖	mathematical	`IsComplete` `SetRel` `Filter` `Filter.instMembership` `uniformity`	`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`	`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` 📖	—	`CauchySeq` `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.Finite` `Set` `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