Compact

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

Statistics

Metric	Count
Definitions	0
Theorems exists_uniform_thickening, exists_uniform_thickening_of_basis, lebesgue_number_lemma, lebesgue_number_lemma_nhds, lebesgue_number_lemma_nhds', lebesgue_number_lemma_nhdsWithin, lebesgue_number_lemma_nhdsWithin', relImage_of_isCompact, relPreimage_of_isCompact, nhdsSet_basis_uniformity, compactSpace_uniformity, lebesgue_number_lemma, lebesgue_number_lemma_nhds, lebesgue_number_lemma_nhds', lebesgue_number_lemma_nhdsWithin, lebesgue_number_lemma_nhdsWithin', lebesgue_number_lemma_sUnion, lebesgue_number_of_compact_open, nhdsSet_diagonal_eq_uniformity, unique_uniformity_of_compact	20
Total	20

Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_uniform_thickening 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Filter Filter.instMembership uniformity Set.iUnion Set.instMembership UniformSpace.ball	—	IsOpen.mem_nhdsSet IsClosed.isOpen_compl le_compl_right Filter.HasBasis.mem_iff IsCompact.nhdsSet_basis_uniformity Filter.basis_sets comp_symm_mem_uniformity_sets Set.disjoint_left Set.mem_iUnion₂_of_mem UniformSpace.mem_comp_of_mem_ball UniformSpace.mem_ball_symmetry
exists_uniform_thickening_of_basis 📖	mathematical	Filter.HasBasis uniformity IsCompact UniformSpace.toTopologicalSpace Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Set.iUnion Set.instMembership UniformSpace.ball	—	exists_uniform_thickening Filter.HasBasis.mem_iff mono Set.iUnion₂_mono UniformSpace.ball_mono

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lebesgue_number_lemma 📖	mathematical	Filter.HasBasis uniformity IsCompact UniformSpace.toTopologicalSpace IsOpen Set Set.instHasSubset Set.iUnion	UniformSpace.ball	—	exists_iff Set.Subset.trans UniformSpace.ball_mono lebesgue_number_lemma
lebesgue_number_lemma_nhds 📖	mathematical	Filter.HasBasis uniformity IsCompact UniformSpace.toTopologicalSpace Set Filter Filter.instMembership nhds	Set.instHasSubset UniformSpace.ball	—	exists_iff Set.Subset.trans UniformSpace.ball_mono lebesgue_number_lemma_nhds
lebesgue_number_lemma_nhds' 📖	mathematical	Filter.HasBasis uniformity IsCompact UniformSpace.toTopologicalSpace Set Filter Filter.instMembership nhds	Set.instHasSubset UniformSpace.ball Set.instMembership	—	exists_iff Set.Subset.trans UniformSpace.ball_mono lebesgue_number_lemma_nhds'
lebesgue_number_lemma_nhdsWithin 📖	mathematical	Filter.HasBasis uniformity IsCompact UniformSpace.toTopologicalSpace Set Filter Filter.instMembership nhdsWithin	Set.instHasSubset Set.instInter UniformSpace.ball	—	exists_iff Set.Subset.trans Set.inter_subset_inter_left UniformSpace.ball_mono lebesgue_number_lemma_nhdsWithin
lebesgue_number_lemma_nhdsWithin' 📖	mathematical	Filter.HasBasis uniformity IsCompact UniformSpace.toTopologicalSpace Set Filter Filter.instMembership nhdsWithin	Set.instHasSubset Set.instInter UniformSpace.ball Set.instMembership	—	exists_iff Set.Subset.trans Set.inter_subset_inter_left UniformSpace.ball_mono lebesgue_number_lemma_nhdsWithin'

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
relImage_of_isCompact 📖	mathematical	IsCompact	IsClosed SetRel.image	—	relPreimage_of_isCompact relInv
relPreimage_of_isCompact 📖	mathematical	IsCompact	IsClosed SetRel.preimage	—	isOpen_compl_iff isOpen_iff_eventually IsCompact.eventually_forall_of_forall_eventually

IsCompact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nhdsSet_basis_uniformity 📖	mathematical	Filter.HasBasis uniformity IsCompact UniformSpace.toTopologicalSpace	nhdsSet Set.iUnion Set Set.instMembership UniformSpace.ball	—	Set.iUnion_const Filter.HasBasis.lebesgue_number_lemma isOpen_interior HasSubset.Subset.trans Set.instIsTransSubset interior_subset Filter.mem_of_superset bUnion_mem_nhdsSet UniformSpace.ball_mem_nhds Filter.HasBasis.mem_of_mem

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace_uniformity 📖	mathematical	—	uniformity iSup Filter Filter.instSupSet nhds instTopologicalSpaceProd UniformSpace.toTopologicalSpace	—	nhdsSet_diagonal_eq_uniformity nhdsSet_diagonal
lebesgue_number_lemma 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace IsOpen Set Set.instHasSubset Set.iUnion	Filter Filter.instMembership uniformity UniformSpace.ball	—	Set.mem_iUnion Filter.HasBasis.mem_iff Filter.HasBasis.comap Filter.HasBasis.lift' Filter.basis_sets Monotone.relComp monotone_id lift'_comp_uniformity nhds_eq_comap_uniformity IsOpen.mem_nhds_iff IsCompact.elim_nhds_subcover' UniformSpace.ball_mem_nhds Filter.biInter_finset_mem Set.mem_iUnion₂ Set.mem_iInter₂
lebesgue_number_lemma_nhds 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace Set Filter Filter.instMembership nhds	uniformity Set.instHasSubset UniformSpace.ball	—	lebesgue_number_lemma isOpen_interior Set.mem_iUnion mem_interior_iff_mem_nhds HasSubset.Subset.trans Set.instIsTransSubset interior_subset
lebesgue_number_lemma_nhds' 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace Set Filter Filter.instMembership nhds	uniformity Set.instHasSubset UniformSpace.ball Set.instMembership	—	lebesgue_number_lemma isOpen_interior Set.mem_iUnion mem_interior_iff_mem_nhds HasSubset.Subset.trans Set.instIsTransSubset interior_subset
lebesgue_number_lemma_nhdsWithin 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace Set Filter Filter.instMembership nhdsWithin	uniformity Set.instHasSubset Set.instInter UniformSpace.ball	—	Set.inter_subset lebesgue_number_lemma_nhds Filter.mem_inf_principal'
lebesgue_number_lemma_nhdsWithin' 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace Set Filter Filter.instMembership nhdsWithin	uniformity Set.instHasSubset Set.instInter UniformSpace.ball Set.instMembership	—	Set.inter_subset lebesgue_number_lemma_nhds' Filter.mem_inf_principal'
lebesgue_number_lemma_sUnion 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace IsOpen Set Set.instHasSubset Set.sUnion	Filter Filter.instMembership uniformity Set.instMembership UniformSpace.ball	—	lebesgue_number_lemma Set.sUnion_eq_iUnion
lebesgue_number_of_compact_open 📖	mathematical	IsCompact UniformSpace.toTopologicalSpace IsOpen Set Set.instHasSubset	Filter Filter.instMembership uniformity instTopologicalSpaceProd UniformSpace.ball	—	Filter.HasBasis.mem_iff IsCompact.nhdsSet_basis_uniformity uniformity_hasBasis_open IsOpen.mem_nhdsSet Set.iUnion₂_subset_iff
nhdsSet_diagonal_eq_uniformity 📖	mathematical	—	nhdsSet instTopologicalSpaceProd UniformSpace.toTopologicalSpace Set.diagonal uniformity	—	LE.le.antisymm nhdsSet_diagonal_le_uniformity uniformity_prod_eq_comap_prod Filter.HasBasis.comap Filter.HasBasis.prod_self Filter.basis_sets Filter.HasBasis.ge_iff IsCompact.nhdsSet_basis_uniformity isCompact_diagonal Filter.mem_of_superset Set.mem_iUnion₂ refl_mem_uniformity
unique_uniformity_of_compact 📖	—	UniformSpace.toTopologicalSpace	—	—	UniformSpace.ext compactSpace_uniformity

---

← Back to Index