CompactlyGeneratedSpace

📁 Source: Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean

Statistics

Metric	Count
Definitions `CompactlyGeneratedSpace`, `compactlyGenerated`, `UCompactlyGeneratedSpace`	3
Theorems `isClosed`, `isClosed'`, `isClosed_iff_of_t2`, `isOpen`, `isOpen'`, `isClosed`, `isOpen`, `le_compactlyGenerated`, `compactlyGeneratedSpace_of_coinduced`, `compactlyGeneratedSpace_of_continuous_maps`, `compactlyGeneratedSpace_of_isClosed`, `compactlyGeneratedSpace_of_isClosed_of_t2`, `compactlyGeneratedSpace_of_isOpen`, `compactlyGeneratedSpace_of_isOpen_of_t2`, `continuous_from_compactlyGenerated`, `continuous_from_compactlyGeneratedSpace`, `continuous_from_uCompactlyGeneratedSpace`, `eq_compactlyGenerated`, `instCompactlyGeneratedSpaceOfWeaklyLocallyCompactSpace`, `instCompactlyGeneratedSpaceSigma`, `instUCompactlyGeneratedSpaceOfDiscreteTopology`, `instUCompactlyGeneratedSpaceOfSequentialSpace`, `instUCompactlyGeneratedSpaceQuotient`, `instUCompactlyGeneratedSpaceSigma`, `instUCompactlyGeneratedSpaceSum`, `of_compactlyCoherentSpace_of_t2`, `to_compactlyCoherentSpace`, `uCompactlyGeneratedSpace_of_coinduced`, `uCompactlyGeneratedSpace_of_continuous_maps`, `uCompactlyGeneratedSpace_of_isClosed`, `uCompactlyGeneratedSpace_of_isOpen`	31
Total	34

CompactlyGeneratedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosed` 📖	—	`IsClosed` `Set` `Set.instInter`	—	—	`isClosed'` `Set.preimage_inter_range` `IsClosed.preimage` `isCompact_range`
`isClosed'` 📖	—	`IsClosed` `Set.preimage`	—	—	`UCompactlyGeneratedSpace.isClosed` `CompHaus.instCompactSpaceCarrierToTopTrue` `CompHaus.instT2SpaceCarrierToTopTrue`
`isClosed_iff_of_t2` 📖	mathematical	—	`IsClosed` `Set` `Set.instInter`	—	`IsClosed.inter` `IsCompact.isClosed` `isClosed`
`isOpen` 📖	—	`IsOpen` `Set` `Set.instInter`	—	—	`isOpen'` `Set.preimage_inter_range` `IsOpen.preimage` `isCompact_range`
`isOpen'` 📖	—	`IsOpen` `Set.preimage`	—	—	`UCompactlyGeneratedSpace.isOpen` `CompHaus.instCompactSpaceCarrierToTopTrue` `CompHaus.instT2SpaceCarrierToTopTrue`

TopologicalSpace

Definitions

Name	Category	Theorems
`compactlyGenerated` 📖	CompOp	3 math math: `UCompactlyGeneratedSpace.le_compactlyGenerated`, `continuous_from_compactlyGenerated`, `eq_compactlyGenerated`

UCompactlyGeneratedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosed` 📖	—	`IsClosed` `TopCat.carrier` `CompHausLike.toTop` `TopCat.str` `Set.preimage` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike`	—	—	`eq_compactlyGenerated` `TopologicalSpace.compactlyGenerated.eq_1` `isClosed_coinduced` `isClosed_sigma_iff`
`isOpen` 📖	—	`IsOpen` `TopCat.carrier` `CompHausLike.toTop` `TopCat.str` `Set.preimage` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike`	—	—	`eq_compactlyGenerated` `TopologicalSpace.compactlyGenerated.eq_1` `isOpen_coinduced` `isOpen_sigma_iff`
`le_compactlyGenerated` 📖	mathematical	—	`TopologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.instPartialOrder` `TopologicalSpace.compactlyGenerated`	—	—

(root)

Definitions

Name	Category	Theorems
`CompactlyGeneratedSpace` 📖	MathDef	8 math math: `compactlyGeneratedSpace_of_isOpen`, `compactlyGeneratedSpace_of_coinduced`, `instCompactlyGeneratedSpaceOfWeaklyLocallyCompactSpace`, `of_compactlyCoherentSpace_of_t2`, `compactlyGeneratedSpace_of_isClosed_of_t2`, `compactlyGeneratedSpace_of_isClosed`, `compactlyGeneratedSpace_of_continuous_maps`, `compactlyGeneratedSpace_of_isOpen_of_t2`
`UCompactlyGeneratedSpace` 📖	CompData	11 math math: `CondensedSet.instUCompactlyGeneratedSpaceCarrierToTopCat`, `instUCompactlyGeneratedSpaceOfDiscreteTopology`, `uCompactlyGeneratedSpace_of_isOpen`, `uCompactlyGeneratedSpace_of_continuous_maps`, `CondensedSet.instUCompactlyGeneratedSpaceCarrierObjTopCatCondensedSetToTopCat`, `uCompactlyGeneratedSpace_of_coinduced`, `CompactlyGenerated.is_compactly_generated`, `instUCompactlyGeneratedSpaceOfSequentialSpace`, `uCompactlyGeneratedSpace_of_isClosed`, `instUCompactlyGeneratedSpaceQuotient`, `instUCompactlyGeneratedSpaceSum`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compactlyGeneratedSpace_of_coinduced` 📖	mathematical	`Continuous` `TopologicalSpace.coinduced`	`CompactlyGeneratedSpace`	—	`uCompactlyGeneratedSpace_of_coinduced`
`compactlyGeneratedSpace_of_continuous_maps` 📖	mathematical	`Continuous`	`CompactlyGeneratedSpace`	—	`uCompactlyGeneratedSpace_of_continuous_maps`
`compactlyGeneratedSpace_of_isClosed` 📖	mathematical	`IsClosed`	`CompactlyGeneratedSpace`	—	`uCompactlyGeneratedSpace_of_isClosed`
`compactlyGeneratedSpace_of_isClosed_of_t2` 📖	mathematical	`IsClosed`	`CompactlyGeneratedSpace`	—	`compactlyGeneratedSpace_of_isClosed` `Set.inter_comm` `Subtype.image_preimage_coe` `IsClosed.isClosedMap_subtype_val` `IsCompact.isClosed` `isCompact_iff_compactSpace` `instT2SpaceSubtype` `continuous_subtype_val`
`compactlyGeneratedSpace_of_isOpen` 📖	mathematical	`IsOpen`	`CompactlyGeneratedSpace`	—	`uCompactlyGeneratedSpace_of_isOpen`
`compactlyGeneratedSpace_of_isOpen_of_t2` 📖	mathematical	`IsOpen`	`CompactlyGeneratedSpace`	—	`compactlyGeneratedSpace_of_isOpen` `isCompact_iff_compactSpace` `instT2SpaceSubtype` `continuous_subtype_val`
`continuous_from_compactlyGenerated` 📖	mathematical	`Continuous` `TopCat.carrier` `CompHausLike.toTop` `TopCat.str` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike`	`TopologicalSpace.compactlyGenerated`	—	`continuous_coinduced_dom`
`continuous_from_compactlyGeneratedSpace` 📖	—	`Continuous`	—	—	`continuous_from_uCompactlyGeneratedSpace` `CompHaus.instCompactSpaceCarrierToTopTrue` `CompHaus.instT2SpaceCarrierToTopTrue`
`continuous_from_uCompactlyGeneratedSpace` 📖	—	`Continuous` `TopCat.carrier` `CompHausLike.toTop` `TopCat.str` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike`	—	—	`continuous_le_dom` `UCompactlyGeneratedSpace.le_compactlyGenerated` `continuous_from_compactlyGenerated`
`eq_compactlyGenerated` 📖	mathematical	—	`TopologicalSpace.compactlyGenerated`	—	`le_antisymm` `UCompactlyGeneratedSpace.le_compactlyGenerated` `ContinuousMap.continuous_toFun`
`instCompactlyGeneratedSpaceOfWeaklyLocallyCompactSpace` 📖	mathematical	—	`CompactlyGeneratedSpace`	—	`compactlyGeneratedSpace_of_isClosed_of_t2` `isClosed_iff_forall_filter` `WeaklyLocallyCompactSpace.exists_compact_mem_nhds` `Set.mem_of_mem_inter_left` `le_inf` `le_trans` `Filter.le_principal_iff` `Filter.inf_principal`
`instCompactlyGeneratedSpaceSigma` 📖	mathematical	`CompactlyGeneratedSpace`	`instTopologicalSpaceSigma`	—	`compactlyGeneratedSpace_of_isClosed` `isClosed_sigma_iff` `CompactlyGeneratedSpace.isClosed'` `Continuous.comp` `continuous_sigmaMk` `continuous_uliftDown` `IsClosed.preimage` `continuous_uliftUp` `ULift.compactSpace` `ULift.instT2Space`
`instUCompactlyGeneratedSpaceOfDiscreteTopology` 📖	mathematical	—	`UCompactlyGeneratedSpace`	—	`DiscreteTopology.eq_bot` `bot_le`
`instUCompactlyGeneratedSpaceOfSequentialSpace` 📖	mathematical	—	`UCompactlyGeneratedSpace`	—	`uCompactlyGeneratedSpace_of_isClosed` `SequentialSpace.isClosed_of_seq` `Nat.cofinite_eq_atTop` `Filter.cocompact_eq_cofinite` `instDiscreteTopologyNat` `Filter.coclosedCompact_eq_cocompact` `instR1Space` `TopologicalSpace.PseudoMetrizableSpace.regularSpace` `PseudoEMetricSpace.pseudoMetrizableSpace` `OnePoint.tendsto_coe_infty` `IsClosed.mem_of_tendsto` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `ULift.compactSpace` `OnePoint.instCompactSpace` `ULift.instT2Space` `T25Space.t2Space` `T3Space.t25Space` `T4Space.t3Space` `instT4SpaceOfT1SpaceOfNormalSpace` `OnePoint.instT1Space` `T5Space.toT1Space` `OrderTopology.t5Space` `OrderTopology.of_linearLocallyFinite` `OnePoint.instNormalSpaceOfWeaklyLocallyCompactSpaceOfR1Space` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `locallyCompact_of_proper` `Nat.instProperSpace` `Continuous.eval` `ContinuousMap.instContinuousEvalOfLocallyCompactPair` `instLocallyCompactPairOfLocallyCompactSpace` `WeaklyLocallyCompactSpace.locallyCompactSpace` `T3Space.toRegularSpace` `instWeaklyLocallyCompactSpaceOfCompactSpace` `continuous_const` `continuous_uliftDown` `Filter.Tendsto.comp` `Continuous.tendsto` `continuous_uliftUp`
`instUCompactlyGeneratedSpaceQuotient` 📖	mathematical	—	`UCompactlyGeneratedSpace` `instTopologicalSpaceQuotient`	—	`uCompactlyGeneratedSpace_of_coinduced` `continuous_quotient_mk'`
`instUCompactlyGeneratedSpaceSigma` 📖	mathematical	`UCompactlyGeneratedSpace`	`instTopologicalSpaceSigma`	—	`uCompactlyGeneratedSpace_of_isClosed` `isClosed_sigma_iff` `UCompactlyGeneratedSpace.isClosed` `Continuous.comp` `continuous_sigmaMk`
`instUCompactlyGeneratedSpaceSum` 📖	mathematical	—	`UCompactlyGeneratedSpace` `instTopologicalSpaceSum`	—	`uCompactlyGeneratedSpace_of_isClosed` `isClosed_sum_iff` `UCompactlyGeneratedSpace.isClosed` `Continuous.comp` `continuous_inl` `continuous_uliftDown` `IsClosed.preimage` `continuous_uliftUp` `ULift.compactSpace` `CompHaus.instCompactSpaceCarrierToTopTrue` `ULift.instT2Space` `CompHaus.instT2SpaceCarrierToTopTrue` `continuous_inr`
`of_compactlyCoherentSpace_of_t2` 📖	mathematical	—	`CompactlyGeneratedSpace`	—	`compactlyGeneratedSpace_of_isClosed_of_t2` `CompactlyCoherentSpace.isClosed_iff` `Subtype.preimage_coe_inter_self` `IsClosed.preimage_val`
`to_compactlyCoherentSpace` 📖	mathematical	—	`CompactlyCoherentSpace`	—	`CompactlyCoherentSpace.of_isOpen_forall_compactSpace` `CompactlyGeneratedSpace.isOpen'`
`uCompactlyGeneratedSpace_of_coinduced` 📖	mathematical	`Continuous` `TopologicalSpace.coinduced`	`UCompactlyGeneratedSpace`	—	`uCompactlyGeneratedSpace_of_isClosed` `isClosed_coinduced` `UCompactlyGeneratedSpace.isClosed` `Continuous.comp`
`uCompactlyGeneratedSpace_of_continuous_maps` 📖	mathematical	`Continuous`	`UCompactlyGeneratedSpace`	—	`continuous_sigma_iff` `continuous_coinduced_rng` `continuous_id_iff_le`
`uCompactlyGeneratedSpace_of_isClosed` 📖	mathematical	`IsClosed`	`UCompactlyGeneratedSpace`	—	`uCompactlyGeneratedSpace_of_continuous_maps` `continuous_iff_isClosed` `IsClosed.preimage`
`uCompactlyGeneratedSpace_of_isOpen` 📖	mathematical	`IsOpen`	`UCompactlyGeneratedSpace`	—	`uCompactlyGeneratedSpace_of_continuous_maps` `continuous_def` `IsOpen.preimage`

---

← Back to Index