SecondCountableSpace

📁 Source: Mathlib/Topology/ContinuousMap/SecondCountableSpace.lean

Statistics

Metric	Count
Definitions	0
Theorems compactOpen_eq_generateFrom, instSecondCountableTopology, instSeparableSpace, secondCountableTopology	4
Total	4

ContinuousMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactOpen_eq_generateFrom 📖	mathematical	IsCompact TopologicalSpace.IsTopologicalBasis Set Set.instMembership Filter Filter.instMembership nhds Set.MapsTo DFunLike.coe ContinuousMap instFunLike	compactOpen TopologicalSpace.generateFrom Set.image2 setOf Set.sUnion Set.Finite Set.instHasSubset	—	le_antisymm TopologicalSpace.generateFrom_anti Set.image2_subset_iff Set.mem_image2_of_mem isOpen_sUnion TopologicalSpace.IsTopologicalBasis.isOpen le_of_nhds_le_nhds nhds_compactOpen TopologicalSpace.nhds_generateFrom IsCompact.elim_finite_subcover_image IsCompact.image ContinuousMapClass.map_continuous instContinuousMapClass Set.sUnion_eq_biUnion Set.mapsTo_iff_image_subset TopologicalSpace.IsTopologicalBasis.open_eq_sUnion' Set.image_subset_iff Set.MapsTo.mono_right Set.subset_sUnion_of_mem IsCompact.elim_nhds_subcover Set.Finite.image Finset.finite_toSet Set.sUnion_image Set.mapsTo_sUnion Set.forall_mem_image Function.sometimes_spec Set.MapsTo.mono Set.sUnion_subset Filter.mem_of_superset Filter.biInter_mem Filter.mem_iInf_of_mem Set.MapsTo.mono_left Filter.mem_principal_self
instSecondCountableTopology 📖	mathematical	—	SecondCountableTopology ContinuousMap compactOpen	—	secondCountableTopology IsOpen.locallyCompactSpace TopologicalSpace.isOpen_of_mem_countableBasis instWeaklyLocallyCompactSpaceOfLocallyCompactSpace sigmaCompactSpace_of_locallyCompact_secondCountable TopologicalSpace.Subtype.secondCountableTopology Set.countable_iUnion Encodable.countable Set.countable_range instCountableNat IsCompact.image CompactExhaustion.isCompact continuous_subtype_val TopologicalSpace.IsTopologicalBasis.mem_nhds_iff TopologicalSpace.isBasis_countableBasis IsOpen.mem_nhds IsOpen.preimage ContinuousMapClass.map_continuous instContinuousMapClass CanLift.prf Subtype.canLift CompactExhaustion.exists_mem_nhds Set.mem_iUnion Set.mem_range_self map_nhds_subtype_coe_eq_nhds Filter.image_mem_map Set.mapsTo_image_iff
instSeparableSpace 📖	mathematical	—	TopologicalSpace.SeparableSpace ContinuousMap compactOpen	—	TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopology
secondCountableTopology 📖	mathematical	Set.Countable Set IsCompact Set.instMembership Filter Filter.instMembership nhds Set.MapsTo DFunLike.coe ContinuousMap instFunLike	SecondCountableTopology compactOpen	—	Set.Countable.image2 Set.countable_setOf_finite_subset TopologicalSpace.countable_countableBasis compactOpen_eq_generateFrom TopologicalSpace.isBasis_countableBasis TopologicalSpace.isOpen_of_mem_countableBasis

---

← Back to Index