Compacts

📁 Source: Mathlib/Topology/Sets/Compacts.lean

Statistics

Metric	Count
Definitions `CompactOpens`, `instBooleanAlgebra`, `instBot`, `instBoundedOrder`, `instCompl`, `instGeneralizedBooleanAlgebra`, `instHImp`, `instInf`, `instInhabited`, `instMax`, `instOrderBot`, `instPartialOrder`, `instSDiff`, `instSProdProd`, `instSemilatticeInf`, `instSemilatticeSup`, `instSetLike`, `instTop`, `map`, `prod`, `toClopens`, `toCompacts`, `toOpens`, `Compacts`, `carrier`, `equiv`, `instBot`, `instBoundedOrderOfCompactSpace`, `instDistribLatticeOfT2Space`, `instInhabited`, `instMax`, `instMinOfT2Space`, `instOrderBot`, `instPartialOrder`, `instSProdProd`, `instSemilatticeSup`, `instSetLike`, `instSingleton`, `instTopOfCompactSpace`, `instUniqueOfIsEmpty`, `map`, `prod`, `toCloseds`, `NonemptyCompacts`, `instInhabited`, `instMax`, `instOrderTopOfCompactSpaceOfNonempty`, `instPartialOrder`, `instSProdProd`, `instSemilatticeSup`, `instSetLike`, `instSingleton`, `instTopOfCompactSpaceOfNonempty`, `instUnique`, `map`, `prod`, `toCloseds`, `toCompacts`, `PositiveCompacts`, `instInhabitedOfCompactSpaceOfNonempty`, `instMax`, `instOrderTopOfCompactSpaceOfNonempty`, `instPartialOrder`, `instSProdProd`, `instSemilatticeSup`, `instSetLike`, `instTopOfCompactSpaceOfNonempty`, `map`, `prod`, `toCompacts`, `toNonemptyCompacts`	71
Theorems `exists_positiveCompacts_closure_subset`, `coe_bot`, `coe_compl`, `coe_finsetSup`, `coe_himp`, `coe_inf`, `coe_map`, `coe_mk`, `coe_prod`, `coe_sdiff`, `coe_sup`, `coe_toClopens`, `coe_toOpens`, `coe_top`, `ext`, `ext_iff`, `isCompact`, `isOpen`, `isOpen'`, `map_comp`, `map_id`, `map_toCompacts`, `toCompacts_map`, `carrier_eq_coe`, `coe_bot`, `coe_eq_empty`, `coe_equiv_apply_eq_preimage`, `coe_finset_sup`, `coe_inf`, `coe_map`, `coe_mk`, `coe_nonempty`, `coe_prod`, `coe_singleton`, `coe_sup`, `coe_toCloseds`, `coe_top`, `equiv_apply`, `equiv_refl`, `equiv_symm`, `equiv_symm_apply`, `equiv_trans`, `ext`, `ext_iff`, `instCanLiftSetCoeIsCompact`, `instCompactSpaceSubtypeMem`, `instNontrivialOfNonempty`, `isCompact`, `isCompact'`, `map_comp`, `map_id`, `map_injective`, `map_injective_iff`, `map_singleton`, `mem_singleton`, `mem_toCloseds`, `nontrivial_iff`, `range_map`, `singleton_inj`, `singleton_injective`, `singleton_prod_singleton`, `subsingleton_iff`, `toCloseds_injective`, `toCloseds_singleton`, `carrier_eq_coe`, `coe_map`, `coe_mk`, `coe_prod`, `coe_singleton`, `coe_sup`, `coe_toCloseds`, `coe_toCompacts`, `coe_top`, `ext`, `ext_iff`, `instIsEmpty`, `instNonempty`, `instNontrivial`, `instSubsingleton`, `isCompact`, `isEmpty_iff`, `map_comp`, `map_id`, `map_injective`, `map_injective_iff`, `map_singleton`, `mem_singleton`, `mem_toCloseds`, `mem_toCompacts`, `nonempty`, `nonempty'`, `nonempty_iff`, `nontrivial_iff`, `range_map`, `range_toCompacts`, `singleton_inj`, `singleton_injective`, `singleton_prod_singleton`, `subsingleton_iff`, `toCloseds_injective`, `toCloseds_singleton`, `toCloseds_toCompacts`, `toCompactSpace`, `toCompacts_injective`, `toCompacts_map`, `toCompacts_singleton`, `toNonempty`, `carrier_eq_coe`, `coe_map`, `coe_mk`, `coe_prod`, `coe_sup`, `coe_toCompacts`, `coe_top`, `ext`, `ext_iff`, `interior_nonempty`, `interior_nonempty'`, `isCompact`, `map_comp`, `map_id`, `nonempty`, `nonempty'`, `exists_positiveCompacts_subset`	124
Total	195

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_positiveCompacts_closure_subset` 📖	mathematical	`IsOpen` `Set.Nonempty`	`Set` `Set.instHasSubset` `closure` `SetLike.coe` `TopologicalSpace.PositiveCompacts` `TopologicalSpace.PositiveCompacts.instSetLike`	—	`exists_positiveCompacts_subset` `IsCompact.closure_subset_of_isOpen` `TopologicalSpace.PositiveCompacts.isCompact`

TopologicalSpace

Definitions

Name	Category	Theorems
`CompactOpens` 📖	CompData	16 math math: `CompactOpens.isCompact`, `CompactOpens.coe_sdiff`, `CompactOpens.coe_toClopens`, `CompactOpens.coe_bot`, `CompactOpens.coe_mk`, `CompactOpens.coe_inf`, `CompactOpens.coe_compl`, `CompactOpens.isOpen`, `CompactOpens.coe_map`, `CompactOpens.coe_prod`, `CompactOpens.coe_finsetSup`, `CompactOpens.ext_iff`, `CompactOpens.coe_top`, `CompactOpens.coe_toOpens`, `CompactOpens.coe_sup`, `CompactOpens.coe_himp`
`Compacts` 📖	CompData	132 math math: `Compacts.isClosed_subsets_of_isClosed`, `Compacts.map_injective`, `Compacts.toCloseds_singleton`, `MeasureTheory.Content.sup_le`, `Compacts.isEmbedding_coe`, `Compacts.coe_inf`, `Compacts.lipschitz_prod`, `Compacts.isClosed_inter_nonempty_of_isClosed`, `Compacts.coe_toCloseds`, `Compacts.singleton_injective`, `MeasureTheory.Measure.haar.le_index_mul`, `MeasureTheory.Measure.haar.addHaarContent_apply`, `Compacts.edist_eq`, `Compacts.isClopen_singleton_bot`, `MeasureTheory.Content.le_outerMeasure_compacts`, `MeasureTheory.Measure.haar.prehaar_le_index`, `Compacts.uniformContinuous_singleton`, `Compacts.carrier_eq_coe`, `MeasureTheory.Measure.haar.prehaar_sup_le`, `Compacts.lipschitz_sup`, `NonemptyCompacts.mem_toCompacts`, `Compacts.instCanLiftSetCoeIsCompact`, `MeasureTheory.Content.measure_eq_content_of_regular`, `MeasureTheory.Content.lt_top`, `Compacts.instCompactSpace`, `Compacts.coe_map`, `NonemptyCompacts.continuous_toCompacts`, `CompactOpens.coe_mk`, `MeasureTheory.Measure.haar.prehaar_empty`, `MeasureTheory.Content.innerContent_exists_compact`, `MeasureTheory.Measure.haar.le_addIndex_mul`, `Compacts.map_singleton`, `Compacts.compactSpace_iff`, `MeasureTheory.Measure.haar.prehaar_sup_eq`, `Compacts.nontrivial_iff`, `MeasureTheory.Measure.haar.mem_prehaar_empty`, `Compacts.uniformity_def`, `MeasureTheory.Content.outerMeasure_interior_compacts`, `Compacts.singleton_prod_singleton`, `MeasureTheory.Measure.haar.add_prehaar_le_addIndex`, `Compacts.totallyBounded_subsets_of_totallyBounded`, `MeasureTheory.Measure.haar.addHaarContent_self`, `Compacts.continuous_coe`, `Filter.HasBasis.uniformity_compacts`, `Compacts.coe_bot`, `ContDiffMapSupportedIn.zero_on_compl'`, `Compacts.discreteUniformity_iff`, `Compacts.isOpen_inter_nonempty_of_isOpen`, `MeasureTheory.Measure.haar.addCHaar_sup_le`, `ContDiffMapSupportedIn.zero_on_compl`, `Compacts.uniformContinuous_toCloseds`, `MeasureTheory.Measure.haar.addPrehaar_sup_eq`, `Compacts.coe_top`, `IsUniformInducing.compacts_map`, `Compacts.coe_sup`, `Compacts.coe_equiv_apply_eq_preimage`, `Compacts.isUniformEmbedding_toCloseds`, `Compacts.toCloseds_injective`, `MeasureTheory.Content.toFun_eq_toNNReal_apply`, `MeasureTheory.Measure.haar.haarContent_apply`, `Compacts.equiv_trans`, `IsUniformEmbedding.compacts_map`, `Compacts.equiv_symm_apply`, `NonemptyCompacts.toCompacts_singleton`, `MeasureTheory.Measure.haar.haarContent_self`, `Compacts.isometry_singleton`, `ContDiffMapSupportedIn.tsupport_subset`, `Compacts.coe_prod`, `Compacts.coe_singleton`, `Compacts.mem_toCloseds`, `Compacts.instCompactSpaceSubtypeMem`, `MeasureTheory.Measure.haar.is_left_invariant_haarContent`, `Compacts.uniformContinuous_sup`, `NonemptyCompacts.coe_toCompacts`, `MeasureTheory.Measure.haar.mem_addPrehaar_empty`, `Compacts.coe_mk`, `UniformContinuous.compacts_map`, `rieszContentAux_sup_le`, `Compacts.isUniformEmbedding_singleton`, `Compacts.coe_finset_sup`, `NonemptyCompacts.isUniformEmbedding_toCompacts`, `NonemptyCompacts.isOpenEmbedding_toCompacts`, `PositiveCompacts.coe_mk`, `MeasureTheory.Measure.haar.chaar_sup_eq`, `Compacts.mem_singleton`, `Compacts.instNoncompactSpace`, `Compacts.uniformContinuous_coe`, `Compacts.noncompactSpace_iff`, `ContDiffMapSupportedIn.iteratedFDeriv_zero_on_compl`, `MeasureTheory.Measure.haar.chaar_sup_le`, `MeasureTheory.Content.outerMeasure_exists_compact`, `Compacts.instDiscreteUniformity`, `Compacts.isCompact`, `Compacts.coe_eq_empty`, `PositiveCompacts.coe_toCompacts`, `Compacts.continuous_toCloseds`, `Compacts.isUniformEmbedding_coe`, `NonemptyCompacts.toCompacts_injective`, `NonemptyCompacts.coe_mk`, `MeasureTheory.Content.empty`, `MeasureTheory.Content.innerContent_of_isCompact`, `MeasureTheory.Measure.haar.chaar_empty`, `Compacts.equiv_refl`, `MeasureTheory.Measure.haar.addCHaar_sup_eq`, `Compacts.instNontrivialOfNonempty`, `Compacts.isCompact_subsets_of_isCompact`, `ContDiffMapSupportedIn.support_subset`, `NonemptyCompacts.uniformContinuous_toCompacts`, `MeasureTheory.Measure.haar.is_left_invariant_addHaarContent`, `Compacts.isEmbedding_toCloseds`, `Compacts.isOpen_subsets_of_isOpen`, `NonemptyCompacts.isEmbedding_toCompacts`, `Compacts.equiv_apply`, `Compacts.range_map`, `Compacts.map_injective_iff`, `ContinuousMap.instCompactSpaceElemCoeCompacts`, `Compacts.subsingleton_iff`, `Compacts.coe_nonempty`, `MeasureTheory.Measure.haar.addCHaar_empty`, `NonemptyCompacts.isClosedEmbedding_toCompacts`, `MeasureTheory.Measure.haar.addPrehaar_sup_le`, `Compacts.singleton_inj`, `Compacts.isometry_toCloseds`, `NonemptyCompacts.isometry_toCompacts`, `isBigO_norm_restrict_cocompact`, `MeasureTheory.Measure.haar.addPrehaar_empty`, `NonemptyCompacts.range_toCompacts`, `Compacts.ext_iff`, `Compacts.equiv_symm`, `ContDiffMapSupportedInClass.map_zero_on_compl`, `MeasureTheory.Content.sup_le'`, `MeasureTheory.Content.contentRegular_exists_compact`
`NonemptyCompacts` 📖	CompData	97 math math: `NonemptyCompacts.uniformContinuous_toCloseds`, `NonemptyCompacts.coe_top`, `NonemptyCompacts.instNonempty`, `NonemptyCompacts.subsingleton_iff`, `NonemptyCompacts.toCloseds_injective`, `NonemptyCompacts.coe_prod`, `EMetric.NonemptyCompacts.lipschitz_prod`, `EMetric.NonemptyCompacts.isometry_toCloseds`, `NonemptyCompacts.nonempty_iff`, `EMetric.NonemptyCompacts.isUniformEmbedding_toCloseds`, `Filter.HasBasis.uniformity_nonemptyCompacts`, `NonemptyCompacts.isClosed_in_closeds`, `NonemptyCompacts.isometry_singleton`, `NonemptyCompacts.isEmbedding_coe`, `NonemptyCompacts.toCompactSpace`, `NonemptyCompacts.ext_iff`, `NonemptyCompacts.uniformContinuous_coe`, `NonemptyCompacts.mem_toCompacts`, `NonemptyCompacts.continuous_toCompacts`, `NonemptyCompacts.uniformity_def`, `NonemptyCompacts.uniformContinuous_singleton`, `NonemptyCompacts.mem_toCloseds`, `NonemptyCompacts.coe_toCloseds`, `NonemptyCompacts.singleton_prod_singleton`, `NonemptyCompacts.lipschitz_prod`, `NonemptyCompacts.isOpen_inter_nonempty_of_isOpen`, `NonemptyCompacts.instDiscreteUniformity`, `NonemptyCompacts.uniformContinuous_sup`, `Metric.uniformContinuous_infDist_Hausdorff_dist`, `NonemptyCompacts.isEmpty_iff`, `NonemptyCompacts.isEmbedding_toCloseds`, `NonemptyCompacts.isUniformEmbedding_coe`, `NonemptyCompacts.nontrivial_iff`, `NonemptyCompacts.coe_map`, `NonemptyCompacts.isOpen_subsets_of_isOpen`, `NonemptyCompacts.toCompacts_singleton`, `GromovHausdorff.toGHSpace_continuous`, `NonemptyCompacts.instIsEmpty`, `NonemptyCompacts.coe_toCompacts`, `NonemptyCompacts.mem_singleton`, `NonemptyCompacts.isClosed_inter_nonempty_of_isClosed`, `NonemptyCompacts.isUniformEmbedding_toCloseds`, `NonemptyCompacts.coe_sup`, `NonemptyCompacts.coe_singleton`, `GromovHausdorff.eq_toGHSpace`, `NonemptyCompacts.isometry_toCloseds`, `NonemptyCompacts.totallyBounded_subsets_of_totallyBounded`, `NonemptyCompacts.carrier_eq_coe`, `NonemptyCompacts.isUniformEmbedding_toCompacts`, `NonemptyCompacts.isOpenEmbedding_toCompacts`, `GromovHausdorff.ghDist_le_nonemptyCompacts_dist`, `NonemptyCompacts.nonempty`, `NonemptyCompacts.range_map`, `EMetric.NonemptyCompacts.isClosed_in_closeds`, `NonemptyCompacts.isUniformEmbedding_singleton`, `NonemptyCompacts.instCompactSpace`, `NonemptyCompacts.singleton_inj`, `NonemptyCompacts.instCompleteSpace`, `NonemptyCompacts.discreteUniformity_iff`, `NonemptyCompacts.toCompacts_injective`, `NonemptyCompacts.noncompactSpace_iff`, `NonemptyCompacts.lipschitz_sup`, `NonemptyCompacts.map_injective_iff`, `NonemptyCompacts.coe_mk`, `GromovHausdorff.toGHSpace_lipschitz`, `NonemptyCompacts.continuous_toCloseds`, `UniformContinuous.nonemptyCompacts_map`, `EMetric.NonemptyCompacts.ToCloseds.isUniformEmbedding`, `Metric.lipschitz_infDist`, `NonemptyCompacts.uniformContinuous_toCompacts`, `EMetric.NonemptyCompacts.isometry_singleton`, `NonemptyCompacts.isCompact`, `NonemptyCompacts.instNoncompactSpace`, `Metric.lipschitz_infDist_set`, `EMetric.NonemptyCompacts.isClosed_subsets_of_isClosed`, `EMetric.NonemptyCompacts.continuous_toCloseds`, `NonemptyCompacts.continuous_coe`, `NonemptyCompacts.map_singleton`, `NonemptyCompacts.instSubsingleton`, `NonemptyCompacts.isEmbedding_toCompacts`, `NonemptyCompacts.toCloseds_singleton`, `NonemptyCompacts.compactSpace_iff`, `NonemptyCompacts.isCompact_subsets_of_isCompact`, `NonemptyCompacts.singleton_injective`, `NonemptyCompacts.toNonempty`, `NonemptyCompacts.isClosedEmbedding_toCompacts`, `EMetric.NonemptyCompacts.lipschitz_sup`, `NonemptyCompacts.instNontrivial`, `NonemptyCompacts.isometry_toCompacts`, `GromovHausdorff.eq_toGHSpace_iff`, `NonemptyCompacts.map_injective`, `NonemptyCompacts.range_toCompacts`, `NonemptyCompacts.isClosed_subsets_of_isClosed`, `IsUniformInducing.nonemptyCompacts_map`, `NonemptyCompacts.instSecondCountableTopology`, `IsUniformEmbedding.nonemptyCompacts_map`, `Metric.NonemptyCompacts.dist_eq`
`PositiveCompacts` 📖	CompData	63 math math: `MeasureTheory.Measure.haar.nonempty_iInter_clAddPrehaar`, `PositiveCompacts.coe_top`, `MeasureTheory.Measure.haarMeasure_closure_self`, `MeasureTheory.Measure.haarMeasure_apply`, `MeasureTheory.Measure.haarMeasure_unique`, `MeasureTheory.Measure.haar.addCHaar_mem_clAddPrehaar`, `MeasureTheory.Measure.haar.le_index_mul`, `MeasureTheory.Measure.haar.addHaarContent_outerMeasure_self_pos`, `MeasureTheory.Measure.haarMeasure_self`, `PositiveCompacts.carrier_eq_coe`, `MeasureTheory.Measure.haar.prehaar_le_index`, `MeasureTheory.Measure.haar.addHaarContent_outerMeasure_closure_pos`, `MeasureTheory.Measure.addHaarMeasure_closure_self`, `PositiveCompacts.ext_iff`, `MeasureTheory.Measure.haar.prehaar_sup_le`, `PositiveCompacts.coe_map`, `MeasureTheory.Measure.haar.prehaar_pos`, `MeasureTheory.Measure.haar.prehaar_empty`, `MeasureTheory.Measure.haar.le_addIndex_mul`, `MeasureTheory.Measure.haar.prehaar_sup_eq`, `MeasureTheory.Measure.addHaarMeasure_eq_iff`, `MeasureTheory.Measure.haar.add_prehaar_le_addIndex`, `PositiveCompacts.interior_nonempty`, `MeasureTheory.Measure.addHaarMeasure_unique`, `MeasureTheory.Measure.haar.prehaar_nonneg`, `MeasureTheory.Measure.haar.addPrehaar_sup_eq`, `MeasureTheory.Measure.haar.addPrehaar_mono`, `MeasureTheory.Measure.haar.prehaar_mono`, `MeasureTheory.Measure.addHaarMeasure_apply`, `MeasureTheory.Measure.addHaarMeasure_self`, `exists_positiveCompacts_subset`, `Module.Basis.prod_parallelepiped`, `Module.Basis.addHaar_eq_iff`, `PositiveCompacts.nonempty'`, `MeasureTheory.Measure.haar.addCHaar_mem_addHaarProduct`, `PositiveCompacts.coe_mk`, `Module.Basis.coe_parallelepiped`, `MeasureTheory.Measure.haar.prehaar_mem_haarProduct`, `MeasureTheory.Measure.haar.chaar_mem_haarProduct`, `MeasureTheory.Measure.haar.nonempty_iInter_clPrehaar`, `PositiveCompacts.coe_toCompacts`, `MeasureTheory.Measure.haar.addPrehaar_nonneg`, `MeasureTheory.Measure.haar.addPrehaar_pos`, `IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_smulHaarMeasure`, `MeasureTheory.Measure.haar.prehaar_self`, `MeasureTheory.Measure.haar.index_pos`, `MeasureTheory.Measure.haar.is_left_invariant_addPrehaar`, `PositiveCompacts.coe_prod`, `MeasureTheory.Measure.haar.addIndex_pos`, `PositiveCompacts.isCompact`, `MeasureTheory.Measure.haar.addPrehaar_mem_addHaarProduct`, `PositiveCompacts.coe_sup`, `MeasureTheory.Measure.haar.haarContent_outerMeasure_closure_pos`, `MeasureTheory.Measure.haar.haarContent_outerMeasure_self_pos`, `MeasureTheory.Measure.haar.addPrehaar_sup_le`, `IsOpen.exists_positiveCompacts_closure_subset`, `MeasureTheory.Measure.haar.chaar_mem_clPrehaar`, `MeasureTheory.Measure.haar.is_left_invariant_prehaar`, `PositiveCompacts.nonempty`, `MeasureTheory.Measure.haar.addPrehaar_self`, `MeasureTheory.Measure.haar.addPrehaar_empty`, `MeasureTheory.Measure.haarMeasure_eq_iff`, `IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_vaddAddHaarMeasure`

TopologicalSpace.CompactOpens

Definitions

Name	Category	Theorems
`instBooleanAlgebra` 📖	CompOp	—
`instBot` 📖	CompOp	1 math math: `coe_bot`
`instBoundedOrder` 📖	CompOp	—
`instCompl` 📖	CompOp	1 math math: `coe_compl`
`instGeneralizedBooleanAlgebra` 📖	CompOp	—
`instHImp` 📖	CompOp	1 math math: `coe_himp`
`instInf` 📖	CompOp	1 math math: `coe_inf`
`instInhabited` 📖	CompOp	—
`instMax` 📖	CompOp	1 math math: `coe_sup`
`instOrderBot` 📖	CompOp	1 math math: `coe_finsetSup`
`instPartialOrder` 📖	CompOp	—
`instSDiff` 📖	CompOp	1 math math: `coe_sdiff`
`instSProdProd` 📖	CompOp	1 math math: `coe_prod`
`instSemilatticeInf` 📖	CompOp	—
`instSemilatticeSup` 📖	CompOp	1 math math: `coe_finsetSup`
`instSetLike` 📖	CompOp	16 math math: `isCompact`, `coe_sdiff`, `coe_toClopens`, `coe_bot`, `coe_mk`, `coe_inf`, `coe_compl`, `isOpen`, `coe_map`, `coe_prod`, `coe_finsetSup`, `ext_iff`, `coe_top`, `coe_toOpens`, `coe_sup`, `coe_himp`
`instTop` 📖	CompOp	1 math math: `coe_top`
`map` 📖	CompOp	5 math math: `map_id`, `coe_map`, `map_comp`, `toCompacts_map`, `map_toCompacts`
`prod` 📖	CompOp	—
`toClopens` 📖	CompOp	1 math math: `coe_toClopens`
`toCompacts` 📖	CompOp	3 math math: `toCompacts_map`, `map_toCompacts`, `isOpen'`
`toOpens` 📖	CompOp	1 math math: `coe_toOpens`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_bot` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.CompactOpens` `instSetLike` `Bot.bot` `instBot` `Set` `Set.instEmptyCollection`	—	—
`coe_compl` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.CompactOpens` `instSetLike` `Compl.compl` `instCompl` `Set` `Set.instCompl`	—	—
`coe_finsetSup` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.CompactOpens` `instSetLike` `Finset.sup` `instSemilatticeSup` `instOrderBot` `Set.iUnion` `Finset` `Finset.instMembership`	—	`Finset.induction_on` `Finset.sup_empty` `Set.iUnion_congr_Prop` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `Finset.sup_insert` `Set.iUnion_iUnion_eq_or_left`
`coe_himp` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.CompactOpens` `instSetLike` `HImp.himp` `instHImp` `Set` `BooleanAlgebra.toHImp` `Set.instBooleanAlgebra`	—	—
`coe_inf` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.CompactOpens` `instSetLike` `instInf` `Set` `Set.instInter`	—	—
`coe_map` 📖	mathematical	`Continuous` `IsOpenMap`	`SetLike.coe` `TopologicalSpace.CompactOpens` `instSetLike` `map` `Set.image`	—	—
`coe_mk` 📖	mathematical	`IsOpen` `TopologicalSpace.Compacts.carrier`	`SetLike.coe` `TopologicalSpace.CompactOpens` `instSetLike` `TopologicalSpace.Compacts` `TopologicalSpace.Compacts.instSetLike`	—	—
`coe_prod` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.CompactOpens` `instTopologicalSpaceProd` `instSetLike` `SProd.sprod` `instSProdProd` `Set` `Set.instSProd`	—	—
`coe_sdiff` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.CompactOpens` `instSetLike` `instSDiff` `Set` `Set.instSDiff`	—	—
`coe_sup` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.CompactOpens` `instSetLike` `instMax` `Set` `Set.instUnion`	—	—
`coe_toClopens` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Clopens` `TopologicalSpace.Clopens.instSetLike` `toClopens` `TopologicalSpace.CompactOpens` `instSetLike`	—	—
`coe_toOpens` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Opens` `TopologicalSpace.Opens.instSetLike` `toOpens` `TopologicalSpace.CompactOpens` `instSetLike`	—	—
`coe_top` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.CompactOpens` `instSetLike` `Top.top` `instTop` `Set.univ`	—	—
`ext` 📖	—	`SetLike.coe` `TopologicalSpace.CompactOpens` `instSetLike`	—	—	`SetLike.ext'`
`ext_iff` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.CompactOpens` `instSetLike`	—	`ext`
`isCompact` 📖	mathematical	—	`IsCompact` `SetLike.coe` `TopologicalSpace.CompactOpens` `instSetLike`	—	`TopologicalSpace.Compacts.isCompact'`
`isOpen` 📖	mathematical	—	`IsOpen` `SetLike.coe` `TopologicalSpace.CompactOpens` `instSetLike`	—	`isOpen'`
`isOpen'` 📖	mathematical	—	`IsOpen` `TopologicalSpace.Compacts.carrier` `toCompacts`	—	—
`map_comp` 📖	mathematical	`Continuous` `IsOpenMap`	`map` `Continuous.comp` `IsOpenMap.comp`	—	`ext` `Continuous.comp` `IsOpenMap.comp` `Set.image_comp`
`map_id` 📖	mathematical	—	`map` `continuous_id` `IsOpenMap.id`	—	`ext` `continuous_id` `IsOpenMap.id` `Set.image_id`
`map_toCompacts` 📖	mathematical	`Continuous` `IsOpenMap`	`toCompacts` `map` `TopologicalSpace.Compacts.map`	—	`toCompacts_map`
`toCompacts_map` 📖	mathematical	`Continuous` `IsOpenMap`	`toCompacts` `map` `TopologicalSpace.Compacts.map`	—	—

TopologicalSpace.Compacts

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	10 math math: `TopologicalSpace.PositiveCompacts.carrier_eq_coe`, `carrier_eq_coe`, `TopologicalSpace.NonemptyCompacts.nonempty'`, `isCompact'`, `TopologicalSpace.PositiveCompacts.interior_nonempty'`, `TopologicalSpace.NonemptyCompacts.carrier_eq_coe`, `MeasureTheory.Measure.haar.addIndex_union_le`, `TopologicalSpace.CompactOpens.isOpen'`, `MeasureTheory.Measure.haar.index_union_le`, `MeasureTheory.Content.contentRegular_exists_compact`
`equiv` 📖	CompOp	6 math math: `coe_equiv_apply_eq_preimage`, `equiv_trans`, `equiv_symm_apply`, `equiv_refl`, `equiv_apply`, `equiv_symm`
`instBot` 📖	CompOp	9 math math: `isClopen_singleton_bot`, `MeasureTheory.Measure.haar.prehaar_empty`, `coe_bot`, `coe_eq_empty`, `MeasureTheory.Content.empty`, `MeasureTheory.Measure.haar.chaar_empty`, `MeasureTheory.Measure.haar.addCHaar_empty`, `MeasureTheory.Measure.haar.addPrehaar_empty`, `TopologicalSpace.NonemptyCompacts.range_toCompacts`
`instBoundedOrderOfCompactSpace` 📖	CompOp	—
`instDistribLatticeOfT2Space` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instMax` 📖	CompOp	18 math math: `MeasureTheory.Content.sup_le`, `MeasureTheory.Measure.haar.prehaar_sup_le`, `lipschitz_sup`, `MeasureTheory.Measure.haar.prehaar_sup_eq`, `MeasureTheory.Content.sup_disjoint'`, `MeasureTheory.Measure.haar.addCHaar_sup_le`, `MeasureTheory.Measure.haar.addPrehaar_sup_eq`, `coe_sup`, `uniformContinuous_sup`, `rieszContentAux_sup_le`, `MeasureTheory.Measure.haar.chaar_sup_eq`, `MeasureTheory.Measure.haar.chaar_sup_le`, `UniformContinuous.sup_compacts`, `MeasureTheory.Measure.haar.addCHaar_sup_eq`, `rieszContentAux_union`, `MeasureTheory.Measure.haar.addPrehaar_sup_le`, `MeasureTheory.Content.sup_disjoint`, `MeasureTheory.Content.sup_le'`
`instMinOfT2Space` 📖	CompOp	1 math math: `coe_inf`
`instOrderBot` 📖	CompOp	1 math math: `coe_finset_sup`
`instPartialOrder` 📖	CompOp	—
`instSProdProd` 📖	CompOp	3 math math: `lipschitz_prod`, `singleton_prod_singleton`, `coe_prod`
`instSemilatticeSup` 📖	CompOp	1 math math: `coe_finset_sup`
`instSetLike` 📖	CompOp	61 math math: `isClosed_subsets_of_isClosed`, `isEmbedding_coe`, `coe_inf`, `isClosed_inter_nonempty_of_isClosed`, `coe_toCloseds`, `MeasureTheory.Measure.haar.le_index_mul`, `edist_eq`, `MeasureTheory.Content.le_outerMeasure_compacts`, `MeasureTheory.Measure.haar.prehaar_le_index`, `carrier_eq_coe`, `TopologicalSpace.NonemptyCompacts.mem_toCompacts`, `instCanLiftSetCoeIsCompact`, `MeasureTheory.Content.measure_eq_content_of_regular`, `coe_map`, `TopologicalSpace.CompactOpens.coe_mk`, `MeasureTheory.Content.innerContent_exists_compact`, `MeasureTheory.Measure.haar.le_addIndex_mul`, `MeasureTheory.Measure.haar.mem_prehaar_empty`, `uniformity_def`, `MeasureTheory.Content.outerMeasure_interior_compacts`, `MeasureTheory.Measure.haar.add_prehaar_le_addIndex`, `totallyBounded_subsets_of_totallyBounded`, `continuous_coe`, `Filter.HasBasis.uniformity_compacts`, `coe_bot`, `ContDiffMapSupportedIn.zero_on_compl'`, `isOpen_inter_nonempty_of_isOpen`, `ContDiffMapSupportedIn.zero_on_compl`, `coe_top`, `coe_sup`, `coe_equiv_apply_eq_preimage`, `ContDiffMapSupportedIn.tsupport_subset`, `coe_prod`, `coe_singleton`, `mem_toCloseds`, `instCompactSpaceSubtypeMem`, `TopologicalSpace.NonemptyCompacts.coe_toCompacts`, `MeasureTheory.Measure.haar.mem_addPrehaar_empty`, `coe_mk`, `coe_finset_sup`, `TopologicalSpace.PositiveCompacts.coe_mk`, `mem_singleton`, `uniformContinuous_coe`, `ContDiffMapSupportedIn.iteratedFDeriv_zero_on_compl`, `MeasureTheory.Content.outerMeasure_exists_compact`, `isCompact`, `coe_eq_empty`, `TopologicalSpace.PositiveCompacts.coe_toCompacts`, `isUniformEmbedding_coe`, `ContinuousMap.norm_restrict_mono_set`, `TopologicalSpace.NonemptyCompacts.coe_mk`, `isCompact_subsets_of_isCompact`, `ContDiffMapSupportedIn.support_subset`, `isOpen_subsets_of_isOpen`, `range_map`, `isCompact_biUnion_coe_of_isCompact`, `ContinuousMap.instCompactSpaceElemCoeCompacts`, `coe_nonempty`, `isBigO_norm_restrict_cocompact`, `ext_iff`, `ContDiffMapSupportedInClass.map_zero_on_compl`
`instSingleton` 📖	CompOp	11 math math: `toCloseds_singleton`, `singleton_injective`, `uniformContinuous_singleton`, `map_singleton`, `singleton_prod_singleton`, `TopologicalSpace.NonemptyCompacts.toCompacts_singleton`, `isometry_singleton`, `coe_singleton`, `isUniformEmbedding_singleton`, `mem_singleton`, `singleton_inj`
`instTopOfCompactSpace` 📖	CompOp	1 math math: `coe_top`
`instUniqueOfIsEmpty` 📖	CompOp	—
`map` 📖	CompOp	21 math math: `map_comp`, `map_injective`, `coe_map`, `map_singleton`, `IsUniformInducing.compacts_map`, `IsUniformEmbedding.compacts_map`, `equiv_symm_apply`, `MeasureTheory.Measure.haar.is_left_invariant_addCHaar`, `MeasureTheory.Measure.haar.is_left_invariant_haarContent`, `UniformContinuous.compacts_map`, `TopologicalSpace.CompactOpens.toCompacts_map`, `TopologicalSpace.CompactOpens.map_toCompacts`, `TopologicalSpace.NonemptyCompacts.toCompacts_map`, `MeasureTheory.Measure.haar.is_left_invariant_chaar`, `MeasureTheory.Measure.haar.is_left_invariant_addHaarContent`, `map_id`, `MeasureTheory.Measure.haar.is_left_invariant_addPrehaar`, `equiv_apply`, `range_map`, `map_injective_iff`, `MeasureTheory.Measure.haar.is_left_invariant_prehaar`
`prod` 📖	CompOp	—
`toCloseds` 📖	CompOp	10 math math: `toCloseds_singleton`, `coe_toCloseds`, `uniformContinuous_toCloseds`, `TopologicalSpace.NonemptyCompacts.toCloseds_toCompacts`, `isUniformEmbedding_toCloseds`, `toCloseds_injective`, `mem_toCloseds`, `continuous_toCloseds`, `isEmbedding_toCloseds`, `isometry_toCloseds`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`carrier_eq_coe` 📖	mathematical	—	`carrier` `SetLike.coe` `TopologicalSpace.Compacts` `instSetLike`	—	—
`coe_bot` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Compacts` `instSetLike` `Bot.bot` `instBot` `Set` `Set.instEmptyCollection`	—	—
`coe_eq_empty` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Compacts` `instSetLike` `Set` `Set.instEmptyCollection` `Bot.bot` `instBot`	—	`SetLike.coe_injective`
`coe_equiv_apply_eq_preimage` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Compacts` `instSetLike` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `Set.preimage` `Homeomorph` `Homeomorph.instEquivLike` `Homeomorph.symm`	—	`Equiv.image_eq_preimage_symm`
`coe_finset_sup` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Compacts` `instSetLike` `Finset.sup` `instSemilatticeSup` `instOrderBot` `Set` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`Finset.cons_induction_on` `Finset.sup_cons`
`coe_inf` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Compacts` `instSetLike` `instMinOfT2Space` `Set` `Set.instInter`	—	—
`coe_map` 📖	mathematical	`Continuous`	`SetLike.coe` `TopologicalSpace.Compacts` `instSetLike` `map` `Set.image`	—	—
`coe_mk` 📖	mathematical	`IsCompact`	`SetLike.coe` `TopologicalSpace.Compacts` `instSetLike`	—	—
`coe_nonempty` 📖	mathematical	—	`Set.Nonempty` `SetLike.coe` `TopologicalSpace.Compacts` `instSetLike`	—	`Set.nonempty_iff_ne_empty` `Iff.not` `coe_eq_empty`
`coe_prod` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Compacts` `instTopologicalSpaceProd` `instSetLike` `SProd.sprod` `instSProdProd` `Set` `Set.instSProd`	—	—
`coe_singleton` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Compacts` `instSetLike` `instSingleton` `Set` `Set.instSingletonSet`	—	—
`coe_sup` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Compacts` `instSetLike` `instMax` `Set` `Set.instUnion`	—	—
`coe_toCloseds` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Closeds` `TopologicalSpace.Closeds.instSetLike` `toCloseds` `TopologicalSpace.Compacts` `instSetLike`	—	—
`coe_top` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Compacts` `instSetLike` `Top.top` `instTopOfCompactSpace` `Set.univ`	—	—
`equiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TopologicalSpace.Compacts` `EquivLike.toFunLike` `Equiv.instEquivLike` `equiv` `map` `Homeomorph` `Homeomorph.instEquivLike` `Homeomorph.continuous`	—	—
`equiv_refl` 📖	mathematical	—	`equiv` `Homeomorph.refl` `Equiv.refl` `TopologicalSpace.Compacts`	—	`Equiv.ext` `map_id`
`equiv_symm` 📖	mathematical	—	`equiv` `Homeomorph.symm` `Equiv.symm` `TopologicalSpace.Compacts`	—	—
`equiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `TopologicalSpace.Compacts` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equiv` `map` `Homeomorph` `Homeomorph.instEquivLike` `Homeomorph.symm`	—	—
`equiv_trans` 📖	mathematical	—	`equiv` `Homeomorph.trans` `Equiv.trans` `TopologicalSpace.Compacts`	—	`Equiv.ext` `map_comp` `Homeomorph.continuous`
`ext` 📖	—	`SetLike.coe` `TopologicalSpace.Compacts` `instSetLike`	—	—	`SetLike.ext'`
`ext_iff` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Compacts` `instSetLike`	—	`ext`
`instCanLiftSetCoeIsCompact` 📖	mathematical	—	`CanLift` `Set` `TopologicalSpace.Compacts` `SetLike.coe` `instSetLike` `IsCompact`	—	—
`instCompactSpaceSubtypeMem` 📖	mathematical	—	`CompactSpace` `TopologicalSpace.Compacts` `SetLike.instMembership` `instSetLike` `instTopologicalSpaceSubtype`	—	`isCompact_iff_compactSpace` `isCompact`
`instNontrivialOfNonempty` 📖	mathematical	—	`Nontrivial` `TopologicalSpace.Compacts`	—	`Set.empty_ne_singleton`
`isCompact` 📖	mathematical	—	`IsCompact` `SetLike.coe` `TopologicalSpace.Compacts` `instSetLike`	—	`isCompact'`
`isCompact'` 📖	mathematical	—	`IsCompact` `carrier`	—	—
`map_comp` 📖	mathematical	`Continuous`	`map` `Continuous.comp`	—	`ext` `Continuous.comp` `Set.image_comp`
`map_id` 📖	mathematical	—	`map` `continuous_id`	—	`ext` `continuous_id` `Set.image_id`
`map_injective` 📖	mathematical	`Continuous`	`TopologicalSpace.Compacts` `map`	—	`Function.Injective.of_comp` `Function.Injective.image_injective` `SetLike.coe_injective`
`map_injective_iff` 📖	mathematical	`Continuous`	`TopologicalSpace.Compacts` `map`	—	`Function.Injective.of_comp` `map_singleton` `singleton_injective` `map_injective`
`map_singleton` 📖	mathematical	`Continuous`	`map` `TopologicalSpace.Compacts` `instSingleton`	—	`ext` `Set.image_singleton`
`mem_singleton` 📖	mathematical	—	`TopologicalSpace.Compacts` `SetLike.instMembership` `instSetLike` `instSingleton`	—	—
`mem_toCloseds` 📖	mathematical	—	`TopologicalSpace.Closeds` `SetLike.instMembership` `TopologicalSpace.Closeds.instSetLike` `toCloseds` `TopologicalSpace.Compacts` `instSetLike`	—	—
`nontrivial_iff` 📖	mathematical	—	`Nontrivial` `TopologicalSpace.Compacts`	—	`not_subsingleton_iff_nontrivial` `subsingleton_iff` `not_isEmpty_iff`
`range_map` 📖	mathematical	`Topology.IsInducing`	`Set.range` `TopologicalSpace.Compacts` `map` `Topology.IsInducing.continuous` `setOf` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`subset_antisymm` `Topology.IsInducing.continuous` `Set.instAntisymmSubset` `Set.range_subset_iff` `Set.image_subset_range` `Topology.IsInducing.isCompact_preimage'` `isCompact` `ext` `Set.image_preimage_eq_of_subset`
`singleton_inj` 📖	mathematical	—	`TopologicalSpace.Compacts` `instSingleton`	—	`singleton_injective`
`singleton_injective` 📖	mathematical	—	`TopologicalSpace.Compacts` `instSingleton`	—	`Function.Injective.of_comp` `Set.singleton_injective`
`singleton_prod_singleton` 📖	mathematical	—	`SProd.sprod` `TopologicalSpace.Compacts` `instTopologicalSpaceProd` `instSProdProd` `instSingleton`	—	`ext` `Set.singleton_prod_singleton`
`subsingleton_iff` 📖	mathematical	—	`TopologicalSpace.Compacts` `IsEmpty`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `instNontrivialOfNonempty` `Unique.instSubsingleton`
`toCloseds_injective` 📖	mathematical	—	`TopologicalSpace.Compacts` `TopologicalSpace.Closeds` `toCloseds`	—	`Function.Injective.of_comp` `SetLike.coe_injective`
`toCloseds_singleton` 📖	mathematical	—	`toCloseds` `TopologicalSpace.Compacts` `instSingleton` `TopologicalSpace.Closeds` `TopologicalSpace.Closeds.instSingletonOfT1Space` `T2Space.t1Space`	—	—

TopologicalSpace.NonemptyCompacts

Definitions

Name	Category	Theorems
`instInhabited` 📖	CompOp	—
`instMax` 📖	CompOp	5 math math: `uniformContinuous_sup`, `coe_sup`, `lipschitz_sup`, `UniformContinuous.sup_nonemptyCompacts`, `EMetric.NonemptyCompacts.lipschitz_sup`
`instOrderTopOfCompactSpaceOfNonempty` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	—
`instSProdProd` 📖	CompOp	4 math math: `coe_prod`, `EMetric.NonemptyCompacts.lipschitz_prod`, `singleton_prod_singleton`, `lipschitz_prod`
`instSemilatticeSup` 📖	CompOp	—
`instSetLike` 📖	CompOp	38 math math: `coe_top`, `coe_prod`, `Filter.HasBasis.uniformity_nonemptyCompacts`, `isEmbedding_coe`, `isCompact_biUnion_coe_of_isCompact`, `toCompactSpace`, `ext_iff`, `uniformContinuous_coe`, `mem_toCompacts`, `uniformity_def`, `mem_toCloseds`, `coe_toCloseds`, `isOpen_inter_nonempty_of_isOpen`, `Metric.uniformContinuous_infDist_Hausdorff_dist`, `isUniformEmbedding_coe`, `coe_map`, `isOpen_subsets_of_isOpen`, `coe_toCompacts`, `mem_singleton`, `isClosed_inter_nonempty_of_isClosed`, `coe_sup`, `coe_singleton`, `GromovHausdorff.eq_toGHSpace`, `totallyBounded_subsets_of_totallyBounded`, `carrier_eq_coe`, `nonempty`, `range_map`, `coe_mk`, `Metric.lipschitz_infDist`, `isCompact`, `Metric.lipschitz_infDist_set`, `EMetric.NonemptyCompacts.isClosed_subsets_of_isClosed`, `continuous_coe`, `isCompact_subsets_of_isCompact`, `toNonempty`, `GromovHausdorff.eq_toGHSpace_iff`, `isClosed_subsets_of_isClosed`, `Metric.NonemptyCompacts.dist_eq`
`instSingleton` 📖	CompOp	12 math math: `isometry_singleton`, `uniformContinuous_singleton`, `singleton_prod_singleton`, `toCompacts_singleton`, `mem_singleton`, `coe_singleton`, `isUniformEmbedding_singleton`, `singleton_inj`, `EMetric.NonemptyCompacts.isometry_singleton`, `map_singleton`, `toCloseds_singleton`, `singleton_injective`
`instTopOfCompactSpaceOfNonempty` 📖	CompOp	1 math math: `coe_top`
`instUnique` 📖	CompOp	—
`map` 📖	CompOp	11 math math: `coe_map`, `toCompacts_map`, `range_map`, `map_id`, `map_injective_iff`, `UniformContinuous.nonemptyCompacts_map`, `map_singleton`, `map_comp`, `map_injective`, `IsUniformInducing.nonemptyCompacts_map`, `IsUniformEmbedding.nonemptyCompacts_map`
`prod` 📖	CompOp	—
`toCloseds` 📖	CompOp	16 math math: `uniformContinuous_toCloseds`, `toCloseds_injective`, `EMetric.NonemptyCompacts.isometry_toCloseds`, `EMetric.NonemptyCompacts.isUniformEmbedding_toCloseds`, `isClosed_in_closeds`, `mem_toCloseds`, `coe_toCloseds`, `isEmbedding_toCloseds`, `toCloseds_toCompacts`, `isUniformEmbedding_toCloseds`, `isometry_toCloseds`, `EMetric.NonemptyCompacts.isClosed_in_closeds`, `continuous_toCloseds`, `EMetric.NonemptyCompacts.ToCloseds.isUniformEmbedding`, `EMetric.NonemptyCompacts.continuous_toCloseds`, `toCloseds_singleton`
`toCompacts` 📖	CompOp	16 math math: `mem_toCompacts`, `continuous_toCompacts`, `nonempty'`, `toCloseds_toCompacts`, `toCompacts_singleton`, `coe_toCompacts`, `carrier_eq_coe`, `isUniformEmbedding_toCompacts`, `isOpenEmbedding_toCompacts`, `toCompacts_map`, `toCompacts_injective`, `uniformContinuous_toCompacts`, `isEmbedding_toCompacts`, `isClosedEmbedding_toCompacts`, `isometry_toCompacts`, `range_toCompacts`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`carrier_eq_coe` 📖	mathematical	—	`TopologicalSpace.Compacts.carrier` `toCompacts` `SetLike.coe` `TopologicalSpace.NonemptyCompacts` `instSetLike`	—	—
`coe_map` 📖	mathematical	`Continuous`	`SetLike.coe` `TopologicalSpace.NonemptyCompacts` `instSetLike` `map` `Set.image`	—	—
`coe_mk` 📖	mathematical	`Set.Nonempty` `TopologicalSpace.Compacts.carrier`	`SetLike.coe` `TopologicalSpace.NonemptyCompacts` `instSetLike` `TopologicalSpace.Compacts` `TopologicalSpace.Compacts.instSetLike`	—	—
`coe_prod` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.NonemptyCompacts` `instTopologicalSpaceProd` `instSetLike` `SProd.sprod` `instSProdProd` `Set` `Set.instSProd`	—	—
`coe_singleton` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.NonemptyCompacts` `instSetLike` `instSingleton` `Set` `Set.instSingletonSet`	—	—
`coe_sup` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.NonemptyCompacts` `instSetLike` `instMax` `Set` `Set.instUnion`	—	—
`coe_toCloseds` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Closeds` `TopologicalSpace.Closeds.instSetLike` `toCloseds` `TopologicalSpace.NonemptyCompacts` `instSetLike`	—	—
`coe_toCompacts` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Compacts` `TopologicalSpace.Compacts.instSetLike` `toCompacts` `TopologicalSpace.NonemptyCompacts` `instSetLike`	—	—
`coe_top` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.NonemptyCompacts` `instSetLike` `Top.top` `instTopOfCompactSpaceOfNonempty` `Set.univ`	—	—
`ext` 📖	—	`SetLike.coe` `TopologicalSpace.NonemptyCompacts` `instSetLike`	—	—	`SetLike.ext'`
`ext_iff` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.NonemptyCompacts` `instSetLike`	—	`ext`
`instIsEmpty` 📖	mathematical	—	`IsEmpty` `TopologicalSpace.NonemptyCompacts`	—	`not_isEmpty_iff` `Set.Nonempty.to_type` `nonempty`
`instNonempty` 📖	mathematical	—	`TopologicalSpace.NonemptyCompacts`	—	`Nonempty.map`
`instNontrivial` 📖	mathematical	—	`Nontrivial` `TopologicalSpace.NonemptyCompacts`	—	`Function.Injective.nontrivial` `singleton_injective`
`instSubsingleton` 📖	mathematical	—	`TopologicalSpace.NonemptyCompacts`	—	`ext` `Subsingleton.eq_univ_of_nonempty` `nonempty`
`isCompact` 📖	mathematical	—	`IsCompact` `SetLike.coe` `TopologicalSpace.NonemptyCompacts` `instSetLike`	—	`TopologicalSpace.Compacts.isCompact'`
`isEmpty_iff` 📖	mathematical	—	`IsEmpty` `TopologicalSpace.NonemptyCompacts`	—	`Function.isEmpty` `instIsEmpty`
`map_comp` 📖	mathematical	`Continuous`	`map` `Continuous.comp`	—	`ext` `Continuous.comp` `Set.ext` `Set.image_congr`
`map_id` 📖	mathematical	—	`map` `continuous_id`	—	`ext` `continuous_id` `Set.ext` `Set.image_congr` `Set.image_id'`
`map_injective` 📖	mathematical	`Continuous`	`TopologicalSpace.NonemptyCompacts` `map`	—	`Function.Injective.of_comp` `Function.Injective.image_injective` `SetLike.coe_injective`
`map_injective_iff` 📖	mathematical	`Continuous`	`TopologicalSpace.NonemptyCompacts` `map`	—	`Function.Injective.of_comp` `singleton_injective` `map_singleton` `map_injective`
`map_singleton` 📖	mathematical	`Continuous`	`map` `TopologicalSpace.NonemptyCompacts` `instSingleton`	—	`ext` `Set.ext` `Set.image_singleton`
`mem_singleton` 📖	mathematical	—	`TopologicalSpace.NonemptyCompacts` `SetLike.instMembership` `instSetLike` `instSingleton`	—	—
`mem_toCloseds` 📖	mathematical	—	`TopologicalSpace.Closeds` `SetLike.instMembership` `TopologicalSpace.Closeds.instSetLike` `toCloseds` `TopologicalSpace.NonemptyCompacts` `instSetLike`	—	—
`mem_toCompacts` 📖	mathematical	—	`TopologicalSpace.Compacts` `SetLike.instMembership` `TopologicalSpace.Compacts.instSetLike` `toCompacts` `TopologicalSpace.NonemptyCompacts` `instSetLike`	—	—
`nonempty` 📖	mathematical	—	`Set.Nonempty` `SetLike.coe` `TopologicalSpace.NonemptyCompacts` `instSetLike`	—	`nonempty'`
`nonempty'` 📖	mathematical	—	`Set.Nonempty` `TopologicalSpace.Compacts.carrier` `toCompacts`	—	—
`nonempty_iff` 📖	mathematical	—	`TopologicalSpace.NonemptyCompacts`	—	—
`nontrivial_iff` 📖	mathematical	—	`Nontrivial` `TopologicalSpace.NonemptyCompacts`	—	—
`range_map` 📖	mathematical	`Topology.IsInducing`	`Set.range` `TopologicalSpace.NonemptyCompacts` `map` `Topology.IsInducing.continuous` `setOf` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike`	—	`subset_antisymm` `Topology.IsInducing.continuous` `Set.instAntisymmSubset` `Set.range_subset_iff` `Set.image_subset_range` `Topology.IsInducing.isCompact_preimage'` `isCompact` `Set.Nonempty.preimage'` `nonempty` `ext` `Set.image_preimage_eq_of_subset`
`range_toCompacts` 📖	mathematical	—	`Set.range` `TopologicalSpace.Compacts` `TopologicalSpace.NonemptyCompacts` `toCompacts` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Bot.bot` `TopologicalSpace.Compacts.instBot`	—	`Set.ext` `Set.mem_compl_singleton_iff` `TopologicalSpace.Compacts.coe_nonempty` `nonempty`
`singleton_inj` 📖	mathematical	—	`TopologicalSpace.NonemptyCompacts` `instSingleton`	—	`singleton_injective`
`singleton_injective` 📖	mathematical	—	`TopologicalSpace.NonemptyCompacts` `instSingleton`	—	`Function.Injective.of_comp` `Set.singleton_injective`
`singleton_prod_singleton` 📖	mathematical	—	`SProd.sprod` `TopologicalSpace.NonemptyCompacts` `instTopologicalSpaceProd` `instSProdProd` `instSingleton`	—	`ext` `Set.singleton_prod_singleton`
`subsingleton_iff` 📖	mathematical	—	`TopologicalSpace.NonemptyCompacts`	—	`Function.Injective.subsingleton` `singleton_injective` `instSubsingleton`
`toCloseds_injective` 📖	mathematical	—	`TopologicalSpace.NonemptyCompacts` `TopologicalSpace.Closeds` `toCloseds`	—	`Function.Injective.of_comp` `SetLike.coe_injective`
`toCloseds_singleton` 📖	mathematical	—	`toCloseds` `TopologicalSpace.NonemptyCompacts` `instSingleton` `TopologicalSpace.Closeds` `TopologicalSpace.Closeds.instSingletonOfT1Space` `T2Space.t1Space`	—	—
`toCloseds_toCompacts` 📖	mathematical	—	`TopologicalSpace.Compacts.toCloseds` `toCompacts` `toCloseds`	—	—
`toCompactSpace` 📖	mathematical	—	`CompactSpace` `TopologicalSpace.NonemptyCompacts` `SetLike.instMembership` `instSetLike` `instTopologicalSpaceSubtype`	—	`isCompact_iff_compactSpace` `isCompact`
`toCompacts_injective` 📖	mathematical	—	`TopologicalSpace.NonemptyCompacts` `TopologicalSpace.Compacts` `toCompacts`	—	`Function.Injective.of_comp` `SetLike.coe_injective`
`toCompacts_map` 📖	mathematical	`Continuous`	`toCompacts` `map` `TopologicalSpace.Compacts.map`	—	—
`toCompacts_singleton` 📖	mathematical	—	`toCompacts` `TopologicalSpace.NonemptyCompacts` `instSingleton` `TopologicalSpace.Compacts` `TopologicalSpace.Compacts.instSingleton`	—	—
`toNonempty` 📖	mathematical	—	`TopologicalSpace.NonemptyCompacts` `SetLike.instMembership` `instSetLike`	—	`Set.Nonempty.to_subtype` `nonempty`

TopologicalSpace.PositiveCompacts

Definitions

Name	Category	Theorems
`instInhabitedOfCompactSpaceOfNonempty` 📖	CompOp	—
`instMax` 📖	CompOp	1 math math: `coe_sup`
`instOrderTopOfCompactSpaceOfNonempty` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	—
`instSProdProd` 📖	CompOp	2 math math: `Module.Basis.prod_parallelepiped`, `coe_prod`
`instSemilatticeSup` 📖	CompOp	—
`instSetLike` 📖	CompOp	61 math math: `MeasureTheory.Measure.haar.nonempty_iInter_clAddPrehaar`, `coe_top`, `MeasureTheory.Measure.haarMeasure_closure_self`, `MeasureTheory.Measure.haarMeasure_apply`, `MeasureTheory.Measure.haarMeasure_unique`, `MeasureTheory.Measure.haar.addCHaar_mem_clAddPrehaar`, `MeasureTheory.Measure.haar.le_index_mul`, `MeasureTheory.Measure.haar.addHaarContent_outerMeasure_self_pos`, `MeasureTheory.Measure.haarMeasure_self`, `carrier_eq_coe`, `MeasureTheory.Measure.haar.prehaar_le_index`, `MeasureTheory.Measure.haar.addHaarContent_outerMeasure_closure_pos`, `MeasureTheory.Measure.addHaarMeasure_closure_self`, `ext_iff`, `MeasureTheory.Measure.haar.prehaar_sup_le`, `coe_map`, `MeasureTheory.Measure.haar.prehaar_pos`, `MeasureTheory.Measure.haar.prehaar_empty`, `MeasureTheory.Measure.haar.le_addIndex_mul`, `MeasureTheory.Measure.haar.prehaar_sup_eq`, `MeasureTheory.Measure.addHaarMeasure_eq_iff`, `MeasureTheory.Measure.haar.add_prehaar_le_addIndex`, `interior_nonempty`, `MeasureTheory.Measure.addHaarMeasure_unique`, `MeasureTheory.Measure.haar.prehaar_nonneg`, `MeasureTheory.Measure.haar.addPrehaar_sup_eq`, `MeasureTheory.Measure.haar.addPrehaar_mono`, `MeasureTheory.Measure.haar.prehaar_mono`, `MeasureTheory.Measure.addHaarMeasure_apply`, `MeasureTheory.Measure.addHaarMeasure_self`, `exists_positiveCompacts_subset`, `Module.Basis.addHaar_eq_iff`, `MeasureTheory.Measure.haar.addCHaar_mem_addHaarProduct`, `coe_mk`, `Module.Basis.coe_parallelepiped`, `MeasureTheory.Measure.haar.prehaar_mem_haarProduct`, `MeasureTheory.Measure.haar.chaar_mem_haarProduct`, `MeasureTheory.Measure.haar.nonempty_iInter_clPrehaar`, `coe_toCompacts`, `MeasureTheory.Measure.haar.addPrehaar_nonneg`, `MeasureTheory.Measure.haar.addPrehaar_pos`, `IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_smulHaarMeasure`, `MeasureTheory.Measure.haar.prehaar_self`, `MeasureTheory.Measure.haar.index_pos`, `MeasureTheory.Measure.haar.is_left_invariant_addPrehaar`, `coe_prod`, `MeasureTheory.Measure.haar.addIndex_pos`, `isCompact`, `MeasureTheory.Measure.haar.addPrehaar_mem_addHaarProduct`, `coe_sup`, `MeasureTheory.Measure.haar.haarContent_outerMeasure_closure_pos`, `MeasureTheory.Measure.haar.haarContent_outerMeasure_self_pos`, `MeasureTheory.Measure.haar.addPrehaar_sup_le`, `IsOpen.exists_positiveCompacts_closure_subset`, `MeasureTheory.Measure.haar.chaar_mem_clPrehaar`, `MeasureTheory.Measure.haar.is_left_invariant_prehaar`, `nonempty`, `MeasureTheory.Measure.haar.addPrehaar_self`, `MeasureTheory.Measure.haar.addPrehaar_empty`, `MeasureTheory.Measure.haarMeasure_eq_iff`, `IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_vaddAddHaarMeasure`
`instTopOfCompactSpaceOfNonempty` 📖	CompOp	1 math math: `coe_top`
`map` 📖	CompOp	5 math math: `map_comp`, `map_id`, `coe_map`, `Module.Basis.parallelepiped_eq_map`, `Module.Basis.parallelepiped_map`
`prod` 📖	CompOp	—
`toCompacts` 📖	CompOp	9 math math: `carrier_eq_coe`, `MeasureTheory.Measure.haar.addHaarContent_self`, `interior_nonempty'`, `MeasureTheory.Measure.haar.haarContent_self`, `MeasureTheory.Measure.haar.chaar_self`, `coe_toCompacts`, `MeasureTheory.Measure.haar.prehaar_self`, `MeasureTheory.Measure.haar.addCHaar_self`, `MeasureTheory.Measure.haar.addPrehaar_self`
`toNonemptyCompacts` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`carrier_eq_coe` 📖	mathematical	—	`TopologicalSpace.Compacts.carrier` `toCompacts` `SetLike.coe` `TopologicalSpace.PositiveCompacts` `instSetLike`	—	—
`coe_map` 📖	mathematical	`Continuous` `IsOpenMap`	`SetLike.coe` `TopologicalSpace.PositiveCompacts` `instSetLike` `map` `Set.image`	—	—
`coe_mk` 📖	mathematical	`Set.Nonempty` `interior` `TopologicalSpace.Compacts.carrier`	`SetLike.coe` `TopologicalSpace.PositiveCompacts` `instSetLike` `TopologicalSpace.Compacts` `TopologicalSpace.Compacts.instSetLike`	—	—
`coe_prod` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.PositiveCompacts` `instTopologicalSpaceProd` `instSetLike` `SProd.sprod` `instSProdProd` `Set` `Set.instSProd`	—	—
`coe_sup` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.PositiveCompacts` `instSetLike` `instMax` `Set` `Set.instUnion`	—	—
`coe_toCompacts` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.Compacts` `TopologicalSpace.Compacts.instSetLike` `toCompacts` `TopologicalSpace.PositiveCompacts` `instSetLike`	—	—
`coe_top` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.PositiveCompacts` `instSetLike` `Top.top` `instTopOfCompactSpaceOfNonempty` `Set.univ`	—	—
`ext` 📖	—	`SetLike.coe` `TopologicalSpace.PositiveCompacts` `instSetLike`	—	—	`SetLike.ext'`
`ext_iff` 📖	mathematical	—	`SetLike.coe` `TopologicalSpace.PositiveCompacts` `instSetLike`	—	`ext`
`interior_nonempty` 📖	mathematical	—	`Set.Nonempty` `interior` `SetLike.coe` `TopologicalSpace.PositiveCompacts` `instSetLike`	—	`interior_nonempty'`
`interior_nonempty'` 📖	mathematical	—	`Set.Nonempty` `interior` `TopologicalSpace.Compacts.carrier` `toCompacts`	—	—
`isCompact` 📖	mathematical	—	`IsCompact` `SetLike.coe` `TopologicalSpace.PositiveCompacts` `instSetLike`	—	`TopologicalSpace.Compacts.isCompact'`
`map_comp` 📖	mathematical	`Continuous` `IsOpenMap`	`map` `Continuous.comp` `IsOpenMap.comp`	—	`ext` `Continuous.comp` `IsOpenMap.comp` `Set.image_comp`
`map_id` 📖	mathematical	—	`map` `continuous_id` `IsOpenMap.id`	—	`ext` `continuous_id` `IsOpenMap.id` `Set.image_id`
`nonempty` 📖	mathematical	—	`Set.Nonempty` `SetLike.coe` `TopologicalSpace.PositiveCompacts` `instSetLike`	—	`Set.Nonempty.mono` `interior_subset` `interior_nonempty`
`nonempty'` 📖	mathematical	—	`TopologicalSpace.PositiveCompacts`	—	`WeaklyLocallyCompactSpace.exists_compact_mem_nhds` `mem_interior_iff_mem_nhds`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_positiveCompacts_subset` 📖	mathematical	`IsOpen` `Set.Nonempty`	`Set` `Set.instHasSubset` `SetLike.coe` `TopologicalSpace.PositiveCompacts` `TopologicalSpace.PositiveCompacts.instSetLike`	—	`exists_compact_subset`

---

← Back to Index