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	14 math math: totallyBounded_sup, totallyBounded_iff_filter, totallyBounded_principal_iff, totallyBounded_bot, TotallyBounded.map, TotallyBounded.mono, totallyBounded_iSup, HasBasis.filter_totallyBounded_iff, TotallyBounded.sup, totallyBounded_comap, totallyBounded_iff_ultrafilter, totallyBounded_map_iff, totallyBounded_biSup, totallyBounded_sSup

(root)

Definitions

Name	Category	Theorems
TotallyBounded 📖	MathDef	54 math math: UniformSpace.hausdorff.isClosed_setOf_totallyBounded, totallyBounded_Ioo, totallyBounded_biUnion, TotallyBounded.subset, Filter.totallyBounded_principal_iff, totallyBounded_empty, Set.Subsingleton.totallyBounded, IsCompact.totallyBounded, Real.totallyBounded_ball, TopologicalSpace.Closeds.isClosed_setOf_totallyBounded, totallyBounded_insert, TopologicalSpace.Compacts.totallyBounded_subsets_of_totallyBounded, totallyBounded_image_iff, GromovHausdorff.totallyBounded, totallyBounded_absConvexHull, totallyBounded_interUnionBalls, TotallyBounded.image, totallyBounded_closure, totallyBounded_union, totallyBounded_neg, totallyBounded_Ioc, totallyBounded_inv, TopologicalSpace.NonemptyCompacts.totallyBounded_subsets_of_totallyBounded, totallyBounded_convexHull, TotallyBounded.union, Rat.totallyBounded_Icc, isCompact_iff_totallyBounded_isComplete, TotallyBounded.insert, Filter.HasBasis.totallyBounded_iff, totallyBounded_of_forall_isSymm, PadicInt.totallyBounded_univ, CauchySeq.totallyBounded_range, Metric.totallyBounded_iff, EMetric.totallyBounded_iff, totallyBounded_iff_subset, TopologicalSpace.Closeds.totallyBounded_subsets_of_totallyBounded, Metric.totallyBounded_of_finite_discretization, Filter.TotallyBounded.totallyBounded_setOf_clusterPt, TotallyBounded.closure, totallyBounded_Ico, totallyBounded_iff_filter, totallyBounded_iUnion, TotallyBounded.powerset_hausdorff, totallyBounded_iff_subset_finite_iUnion_nhds_one, Valued.integer.totallyBounded_iff_finite_residueField, totallyBounded_iff_ultrafilter, IsSeqCompact.totallyBounded, Set.Finite.totallyBounded, totallyBounded_preimage, 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	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 Real.instIsStrictOrderedRing OrderTopology.to_orderClosedTopology instOrderTopologyReal ConditionallyCompleteLinearOrder.toCompactIccSpace IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal 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