Polish

📁 Source: Mathlib/Topology/MetricSpace/Polish.lean

Statistics

Metric	Count
Definitions PolishSpace, IsClopenable, CompleteCopy, inst, instDist, instMetricSpace	6
Theorems iInf, polishSpace_induced, isClopenable, polishSpace, isClopenable, polishSpace, compl, iUnion, exists_nat_nat_continuous_surjective, exists_polishSpace_forall_le, iInf, instENNReal, toIsCompletelyMetrizableSpace, toSecondCountableTopology, dist_eq, dist_val_le_dist, instCompleteSpace, instSecondCountableTopology, instT0Space, polishSpace, instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace	21
Total	27

CompletePseudometrizable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iInf 📖	mathematical	TopologicalSpace T2Space Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder UniformSpace CompleteSpace Filter.IsCountablyGenerated uniformity UniformSpace.toTopologicalSpace	UniformSpace CompleteSpace Filter.IsCountablyGenerated uniformity UniformSpace.toTopologicalSpace iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	CompleteSpace.iInf iInf_uniformity Filter.iInf.isCountablyGenerated UniformSpace.toTopologicalSpace_iInf

Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
polishSpace_induced 📖	mathematical	—	PolishSpace TopologicalSpace.induced DFunLike.coe Equiv EquivLike.toFunLike instEquivLike	—	Topology.IsClosedEmbedding.polishSpace Homeomorph.isClosedEmbedding

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClopenable 📖	mathematical	—	PolishSpace.IsClopenable	—	coinduced_sup coinduced_compose continuous_subtype_val Equiv.induced_symm Equiv.polishSpace_induced instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.instSeparableSpaceSum TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.Subtype.secondCountableTopology PolishSpace.toSecondCountableTopology TopologicalSpace.IsCompletelyMetrizableSpace.sum PolishSpace.toIsCompletelyMetrizableSpace polishSpace IsOpen.polishSpace isOpen_compl mono isOpen_coinduced isOpen_sum_iff Set.preimage_preimage Subtype.coe_preimage_self Subtype.preimage_coe_compl'
polishSpace 📖	mathematical	—	PolishSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	Topology.IsClosedEmbedding.polishSpace isClosedEmbedding_subtypeVal

IsOpen

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClopenable 📖	mathematical	IsOpen	PolishSpace.IsClopenable	—	compl_compl PolishSpace.IsClopenable.compl IsClosed.isClopenable isClosed_compl
polishSpace 📖	mathematical	IsOpen	PolishSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	CanLift.prf TopologicalSpace.Opens.instCanLiftSetCoeIsOpen

PolishSpace

Definitions

Name	Category	Theorems
IsClopenable 📖	MathDef	6 math math: IsOpen.isClopenable, MeasurableSet.isClopenable, IsClopenable.compl, IsClopenable.iUnion, IsClosed.isClopenable, MeasureTheory.isClopenable_iff_measurableSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_nat_nat_continuous_surjective 📖	mathematical	—	Continuous Pi.topologicalSpace instTopologicalSpaceNat	—	exists_nat_nat_continuous_surjective_of_completeSpace toIsCompletelyMetrizableSpace TopologicalSpace.UpgradedIsCompletelyMetrizableSpace.toCompleteSpace toSecondCountableTopology
exists_polishSpace_forall_le 📖	mathematical	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder PolishSpace	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder PolishSpace	—	iInf_le iInf Option.instCountable le_rfl
iInf 📖	mathematical	TopologicalSpace Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder PolishSpace	PolishSpace iInf TopologicalSpace ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice TopologicalSpace.instCompleteLattice	—	CompletePseudometrizable.iInf TopologicalSpace.t2Space_of_metrizableSpace TopologicalSpace.IsCompletelyMetrizableSpace.MetrizableSpace toIsCompletelyMetrizableSpace TopologicalSpace.UpgradedIsCompletelyMetrizableSpace.toCompleteSpace EMetric.instIsCountablyGeneratedUniformity TopologicalSpace.secondCountableTopology_iInf toSecondCountableTopology t1Space_antitone iInf_le T2Space.t1Space instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity
instENNReal 📖	mathematical	—	PolishSpace ENNReal ENNReal.instTopologicalSpace	—	Topology.IsClosedEmbedding.polishSpace instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.Subtype.secondCountableTopology instSecondCountableTopologyReal TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable complete_of_proper proper_of_compact compactSpace_Icc ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal instIsCountablyGeneratedProdElemUniformity EMetric.instIsCountablyGeneratedUniformity Subtype.t0Space T3Space.toT0Space T4Space.t3Space T5Space.toT4Space OrderTopology.t5Space ENNReal.instOrderTopology orderTopology_of_ordConnected Set.ordConnected_Icc Homeomorph.isClosedEmbedding
toIsCompletelyMetrizableSpace 📖	mathematical	—	TopologicalSpace.IsCompletelyMetrizableSpace	—	—
toSecondCountableTopology 📖	mathematical	—	SecondCountableTopology	—	—

PolishSpace.IsClopenable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl 📖	mathematical	PolishSpace.IsClopenable	PolishSpace.IsClopenable Compl.compl Set Set.instCompl	—	IsOpen.isClosed_compl IsClosed.isOpen_compl
iUnion 📖	mathematical	PolishSpace.IsClopenable	PolishSpace.IsClopenable Set.iUnion	—	PolishSpace.exists_polishSpace_forall_le instCountableNat isOpen_iUnion IsOpen.isClopenable LE.le.trans

TopologicalSpace.Opens

Definitions

Name	Category	Theorems
CompleteCopy 📖	CompOp	5 math math: CompleteCopy.dist_eq, CompleteCopy.instCompleteSpace, CompleteCopy.dist_val_le_dist, CompleteCopy.instT0Space, CompleteCopy.instSecondCountableTopology

TopologicalSpace.Opens.CompleteCopy

Definitions

Name	Category	Theorems
inst 📖	CompOp	2 math math: instT0Space, instSecondCountableTopology
instDist 📖	CompOp	2 math math: dist_eq, dist_val_le_dist
instMetricSpace 📖	CompOp	1 math math: instCompleteSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_eq 📖	mathematical	—	Dist.dist TopologicalSpace.Opens.CompleteCopy instDist Real Real.instAdd PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace TopologicalSpace.Opens UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SetLike.instMembership TopologicalSpace.Opens.instSetLike abs Real.lattice Real.instAddGroup Real.instSub DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Metric.infDist Compl.compl Set Set.instCompl SetLike.coe	—	—
dist_val_le_dist 📖	mathematical	—	Real Real.instLE Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace TopologicalSpace.Opens UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SetLike.instMembership TopologicalSpace.Opens.instSetLike TopologicalSpace.Opens.CompleteCopy instDist	—	le_add_of_nonneg_right IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid abs_nonneg covariant_swap_add_of_covariant_add
instCompleteSpace 📖	mathematical	—	CompleteSpace TopologicalSpace.Opens.CompleteCopy PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace instMetricSpace	—	Metric.complete_of_convergent_controlled_sequences Nat.instAtLeastTwoHAddOfNat one_div inv_pow PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.instZeroLEOneClass Real.instIsOrderedRing Real.instNontrivial cauchySeq_of_le_tendsto_0 LE.le.trans dist_val_le_dist LT.lt.le tendsto_pow_atTop_nhds_zero_of_lt_one AddGroup.existsAddOfLE Real.instArchimedean instOrderTopologyReal Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.instAtLeastTwo cauchySeq_tendsto_of_complete tendsto_subtype_rng sub_lt_iff_lt_add IsRightCancelAdd.addRightStrictMono_of_addRightMono instIsRightCancelAddOfAddRightReflectLE contravariant_swap_add_of_contravariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add le_abs_self abs_sub_comm le_add_of_nonneg_left dist_nonneg le_rfl lt_of_le_of_lt div_nonneg zero_le_one Metric.infDist_nonneg IsClosed.notMem_iff_infDist_pos IsOpen.isClosed_compl TopologicalSpace.Opens.isOpen div_le_iff₀' div_le_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Filter.Tendsto.comp Continuous.tendsto Metric.continuous_infDist_pt ge_of_tendsto' instClosedIciTopology OrderTopology.to_orderClosedTopology Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat lt_of_lt_of_le div_pos one_pos NeZero.one
instSecondCountableTopology 📖	mathematical	—	SecondCountableTopology TopologicalSpace.Opens.CompleteCopy inst	—	—
instT0Space 📖	mathematical	—	T0Space TopologicalSpace.Opens.CompleteCopy inst	—	—

Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
polishSpace 📖	mathematical	Topology.IsClosedEmbedding	PolishSpace	—	PolishSpace.toIsCompletelyMetrizableSpace isEmbedding Topology.IsEmbedding.toIsInducing completeSpace_iff_isComplete_range Isometry.isUniformInducing Topology.IsEmbedding.to_isometry IsClosed.isComplete TopologicalSpace.UpgradedIsCompletelyMetrizableSpace.toCompleteSpace isClosed_range instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace TopologicalSpace.SecondCountableTopology.to_separableSpace Topology.IsEmbedding.secondCountableTopology PolishSpace.toSecondCountableTopology TopologicalSpace.IsCompletelyMetrizableSpace.of_completeSpace_metrizable EMetric.instIsCountablyGeneratedUniformity T3Space.toT0Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity

(root)

Definitions

Name	Category	Theorems
PolishSpace 📖	CompData	14 math math: PolishSpace.exists_polishSpace_forall_le, MeasureTheory.analyticSet_iff_exists_polishSpace_range, Measurable.exists_continuous, IsOpen.polishSpace, Topology.IsClosedEmbedding.polishSpace, UpgradedStandardBorel.toPolishSpace, instPolishSpaceEReal, Equiv.polishSpace_induced, StandardBorelSpace.polish, instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace, MeasurableSet.isClopenable', IsClosed.polishSpace, PolishSpace.iInf, PolishSpace.instENNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instPolishSpaceOfSeparableSpaceOfIsCompletelyMetrizableSpace 📖	mathematical	—	PolishSpace	—	UniformSpace.secondCountable_of_separable EMetric.instIsCountablyGeneratedUniformity

---

← Back to Index