TotallyBounded

📁 Source: Mathlib/Analysis/Convex/TotallyBounded.lean

Statistics

Metric	Count
Definitions TotallyBounded, TotallyBounded	2
Theorems totallyBounded_convexHull	1
Total	3

Filter

Definitions

Name	Category	Theorems
TotallyBounded 📖	MathDef	10 math math: totallyBounded_sup, totallyBounded_iff_filter, totallyBounded_principal_iff, totallyBounded_bot, totallyBounded_iSup, HasBasis.filter_totallyBounded_iff, totallyBounded_iff_ultrafilter, totallyBounded_map_iff, totallyBounded_biSup, totallyBounded_sSup

(root)

Definitions

Name	Category	Theorems
TotallyBounded 📖	MathDef	38 math math: totallyBounded_Ioo, totallyBounded_biUnion, Filter.totallyBounded_principal_iff, totallyBounded_empty, Set.Subsingleton.totallyBounded, IsCompact.totallyBounded, Real.totallyBounded_ball, totallyBounded_insert, totallyBounded_image_iff, GromovHausdorff.totallyBounded, totallyBounded_interUnionBalls, totallyBounded_closure, totallyBounded_union, totallyBounded_Ioc, Rat.totallyBounded_Icc, isCompact_iff_totallyBounded_isComplete, Filter.HasBasis.totallyBounded_iff, totallyBounded_of_forall_isSymm, PadicInt.totallyBounded_univ, CauchySeq.totallyBounded_range, Metric.totallyBounded_iff, EMetric.totallyBounded_iff, totallyBounded_iff_subset, Metric.totallyBounded_of_finite_discretization, Filter.TotallyBounded.totallyBounded_setOf_clusterPt, totallyBounded_Ico, totallyBounded_iff_filter, totallyBounded_iUnion, totallyBounded_iff_subset_finite_iUnion_nhds_one, Valued.integer.totallyBounded_iff_finite_residueField, totallyBounded_iff_ultrafilter, IsSeqCompact.totallyBounded, Set.Finite.totallyBounded, totallyBounded_singleton, EMetric.totallyBounded_iff', totallyBounded_iff_subset_finite_iUnion_nhds_zero, totallyBounded_sUnion, totallyBounded_Icc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
totallyBounded_convexHull 📖	mathematical	TotallyBounded	DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid	—	totallyBounded_iff_subset_finite_iUnion_nhds_zero exists_nhds_zero_half IsTopologicalAddGroup.toContinuousAdd IsUniformAddGroup.to_topologicalAddGroup locallyConvexSpace_iff_exists_convex_subset_zero IsCompact.totallyBounded Set.Finite.isCompact_convexHull Set.iUnion_vadd_set convexHull_mono convexHull_add_subset Convex.convexHull_eq Set.add_subset_add_right add_assoc Set.add_subset_add_left Set.add_subset_add Set.add_subset_iff

---

← Back to Index