Snowflaking

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

Statistics

Metric	Count
Definitions Snowflaking, casesOn_toSnowflaking, homeomorph, instBornology, instDist, instEDist, instEMetricSpace, instMetricSpace, instPseudoEMetricSpace, instPseudoMetricSpace, instTopologicalSpace, instUniformSpace, ofSnowflaking, toSnowflaking, uniformEquiv, val	16
Theorems continuous_ofSnowflaking, continuous_toSnowflaking, dist_ofSnowflaking_ofSnowflaking, dist_toSnowflaking_toSnowflaking, ediam_image_ofSnowflaking, ediam_image_toSnowflaking, ediam_preimage_ofSnowflaking, ediam_preimage_toSnowflaking, edist_def, edist_ofSnowflaking_ofSnowflaking, edist_toSnowflaking_toSnowflaking, ext, ext_iff, homeomorph_apply, homeomorph_symm_apply, image_ofSnowflaking_ball, image_ofSnowflaking_closedBall, image_ofSnowflaking_closedEBall, image_ofSnowflaking_eball, image_ofSnowflaking_emetricBall, image_ofSnowflaking_emetricClosedBall, image_ofSnowflaking_eq_preimage, image_ofSnowflaking_image_toSnowflaking, image_toSnowflaking_ball, image_toSnowflaking_closedBall, image_toSnowflaking_closedEBall, image_toSnowflaking_eball, image_toSnowflaking_emetricBall, image_toSnowflaking_emetricClosedBall, image_toSnowflaking_eq_preimage, image_toSnowflaking_image_ofSnowflaking, instSecondCountableTopology, instT0Space, instT2Space, isBounded_image_ofSnowflaking_iff, isBounded_image_toSnowflaking_iff, isBounded_preimage_ofSnowflaking_iff, isBounded_preimage_toSnowflaking_iff, mk_eq_toSnowflaking, ofSnowflaking_comp_toSnowflaking, ofSnowflaking_toSnowflaking, preimage_ofSnowflaking_ball, preimage_ofSnowflaking_closedBall, preimage_ofSnowflaking_closedEBall, preimage_ofSnowflaking_eball, preimage_ofSnowflaking_emetricBall, preimage_ofSnowflaking_emetricClosedBall, preimage_toSnowflaking_ball, preimage_toSnowflaking_closedBall, preimage_toSnowflaking_closedEBall, preimage_toSnowflaking_eball, preimage_toSnowflaking_emetricBall, preimage_toSnowflaking_emetricClosedBall, symm_ofSnowflaking, symm_toSnowflaking, toEquiv_homeomorph, sizeOf_spec, toSnowflaking_comp_ofSnowflaking, toSnowflaking_ofSnowflaking, uniformContinuous_ofSnowflaking, uniformContinuous_toSnowflaking, uniformEquiv_apply, uniformEquiv_symm_apply, uniformEquiv_toEquiv, val_eq_ofSnowflaking	65
Total	81

Metric

Definitions

Name	Category	Theorems
Snowflaking 📖	CompData	63 math math: Snowflaking.symm_ofSnowflaking, Snowflaking.uniformContinuous_ofSnowflaking, Snowflaking.instSecondCountableTopology, Snowflaking.preimage_ofSnowflaking_closedBall, Snowflaking.toSnowflaking.sizeOf_spec, Snowflaking.ofSnowflaking_comp_toSnowflaking, Snowflaking.image_toSnowflaking_emetricClosedBall, Snowflaking.mk_eq_toSnowflaking, Snowflaking.val_eq_ofSnowflaking, Snowflaking.image_ofSnowflaking_eball, Snowflaking.preimage_toSnowflaking_emetricClosedBall, Snowflaking.isBounded_preimage_ofSnowflaking_iff, Snowflaking.image_toSnowflaking_eball, Snowflaking.ediam_image_ofSnowflaking, Snowflaking.uniformEquiv_toEquiv, Snowflaking.image_ofSnowflaking_ball, Snowflaking.instT2Space, Snowflaking.isBounded_image_ofSnowflaking_iff, Snowflaking.image_ofSnowflaking_eq_preimage, Snowflaking.image_ofSnowflaking_closedEBall, Snowflaking.preimage_toSnowflaking_closedBall, Snowflaking.toSnowflaking_ofSnowflaking, Snowflaking.ediam_preimage_ofSnowflaking, Snowflaking.toEquiv_homeomorph, Snowflaking.ofSnowflaking_toSnowflaking, Snowflaking.image_toSnowflaking_eq_preimage, Snowflaking.preimage_toSnowflaking_eball, Snowflaking.symm_toSnowflaking, Snowflaking.preimage_toSnowflaking_closedEBall, Snowflaking.preimage_ofSnowflaking_ball, Snowflaking.continuous_toSnowflaking, Snowflaking.toSnowflaking_comp_ofSnowflaking, Snowflaking.preimage_toSnowflaking_ball, Snowflaking.edist_toSnowflaking_toSnowflaking, Snowflaking.uniformEquiv_symm_apply, Snowflaking.image_toSnowflaking_closedBall, Snowflaking.image_ofSnowflaking_emetricClosedBall, Snowflaking.edist_ofSnowflaking_ofSnowflaking, Snowflaking.preimage_ofSnowflaking_eball, Snowflaking.uniformContinuous_toSnowflaking, Snowflaking.image_toSnowflaking_closedEBall, Snowflaking.edist_def, Snowflaking.preimage_ofSnowflaking_emetricBall, Snowflaking.dist_ofSnowflaking_ofSnowflaking, Snowflaking.isBounded_preimage_toSnowflaking_iff, Snowflaking.image_ofSnowflaking_closedBall, Snowflaking.uniformEquiv_apply, Snowflaking.ediam_preimage_toSnowflaking, Snowflaking.preimage_ofSnowflaking_emetricClosedBall, Snowflaking.homeomorph_symm_apply, Snowflaking.instT0Space, Snowflaking.image_toSnowflaking_image_ofSnowflaking, Snowflaking.image_toSnowflaking_ball, Snowflaking.continuous_ofSnowflaking, Snowflaking.image_ofSnowflaking_image_toSnowflaking, Snowflaking.image_ofSnowflaking_emetricBall, Snowflaking.preimage_ofSnowflaking_closedEBall, Snowflaking.preimage_toSnowflaking_emetricBall, Snowflaking.dist_toSnowflaking_toSnowflaking, Snowflaking.image_toSnowflaking_emetricBall, Snowflaking.ediam_image_toSnowflaking, Snowflaking.homeomorph_apply, Snowflaking.isBounded_image_toSnowflaking_iff

Metric.Snowflaking

Definitions

Name	Category	Theorems
casesOn_toSnowflaking 📖	CompOp	—
homeomorph 📖	CompOp	3 math math: toEquiv_homeomorph, homeomorph_symm_apply, homeomorph_apply
instBornology 📖	CompOp	4 math math: isBounded_preimage_ofSnowflaking_iff, isBounded_image_ofSnowflaking_iff, isBounded_preimage_toSnowflaking_iff, isBounded_image_toSnowflaking_iff
instDist 📖	CompOp	2 math math: dist_ofSnowflaking_ofSnowflaking, dist_toSnowflaking_toSnowflaking
instEDist 📖	CompOp	3 math math: edist_toSnowflaking_toSnowflaking, edist_ofSnowflaking_ofSnowflaking, edist_def
instEMetricSpace 📖	CompOp	—
instMetricSpace 📖	CompOp	—
instPseudoEMetricSpace 📖	CompOp	20 math math: image_toSnowflaking_emetricClosedBall, image_ofSnowflaking_eball, preimage_toSnowflaking_emetricClosedBall, image_toSnowflaking_eball, ediam_image_ofSnowflaking, image_ofSnowflaking_closedEBall, ediam_preimage_ofSnowflaking, preimage_toSnowflaking_eball, preimage_toSnowflaking_closedEBall, image_ofSnowflaking_emetricClosedBall, preimage_ofSnowflaking_eball, image_toSnowflaking_closedEBall, preimage_ofSnowflaking_emetricBall, ediam_preimage_toSnowflaking, preimage_ofSnowflaking_emetricClosedBall, image_ofSnowflaking_emetricBall, preimage_ofSnowflaking_closedEBall, preimage_toSnowflaking_emetricBall, image_toSnowflaking_emetricBall, ediam_image_toSnowflaking
instPseudoMetricSpace 📖	CompOp	8 math math: preimage_ofSnowflaking_closedBall, image_ofSnowflaking_ball, preimage_toSnowflaking_closedBall, preimage_ofSnowflaking_ball, preimage_toSnowflaking_ball, image_toSnowflaking_closedBall, image_ofSnowflaking_closedBall, image_toSnowflaking_ball
instTopologicalSpace 📖	CompOp	8 math math: instSecondCountableTopology, instT2Space, toEquiv_homeomorph, continuous_toSnowflaking, homeomorph_symm_apply, instT0Space, continuous_ofSnowflaking, homeomorph_apply
instUniformSpace 📖	CompOp	5 math math: uniformContinuous_ofSnowflaking, uniformEquiv_toEquiv, uniformEquiv_symm_apply, uniformContinuous_toSnowflaking, uniformEquiv_apply
ofSnowflaking 📖	CompOp	41 math math: symm_ofSnowflaking, uniformContinuous_ofSnowflaking, preimage_ofSnowflaking_closedBall, ofSnowflaking_comp_toSnowflaking, val_eq_ofSnowflaking, image_ofSnowflaking_eball, preimage_toSnowflaking_emetricClosedBall, isBounded_preimage_ofSnowflaking_iff, ediam_image_ofSnowflaking, uniformEquiv_toEquiv, image_ofSnowflaking_ball, isBounded_image_ofSnowflaking_iff, image_ofSnowflaking_eq_preimage, image_ofSnowflaking_closedEBall, preimage_toSnowflaking_closedBall, toSnowflaking_ofSnowflaking, ediam_preimage_ofSnowflaking, toEquiv_homeomorph, ofSnowflaking_toSnowflaking, image_toSnowflaking_eq_preimage, preimage_toSnowflaking_eball, symm_toSnowflaking, preimage_toSnowflaking_closedEBall, preimage_ofSnowflaking_ball, toSnowflaking_comp_ofSnowflaking, preimage_toSnowflaking_ball, image_ofSnowflaking_emetricClosedBall, edist_ofSnowflaking_ofSnowflaking, preimage_ofSnowflaking_eball, edist_def, preimage_ofSnowflaking_emetricBall, dist_ofSnowflaking_ofSnowflaking, image_ofSnowflaking_closedBall, preimage_ofSnowflaking_emetricClosedBall, image_toSnowflaking_image_ofSnowflaking, continuous_ofSnowflaking, image_ofSnowflaking_image_toSnowflaking, image_ofSnowflaking_emetricBall, preimage_ofSnowflaking_closedEBall, preimage_toSnowflaking_emetricBall, homeomorph_apply
toSnowflaking 📖	CompOp	40 math math: symm_ofSnowflaking, preimage_ofSnowflaking_closedBall, toSnowflaking.sizeOf_spec, ofSnowflaking_comp_toSnowflaking, image_toSnowflaking_emetricClosedBall, mk_eq_toSnowflaking, preimage_toSnowflaking_emetricClosedBall, image_toSnowflaking_eball, image_ofSnowflaking_eq_preimage, preimage_toSnowflaking_closedBall, toSnowflaking_ofSnowflaking, ofSnowflaking_toSnowflaking, image_toSnowflaking_eq_preimage, preimage_toSnowflaking_eball, symm_toSnowflaking, preimage_toSnowflaking_closedEBall, preimage_ofSnowflaking_ball, continuous_toSnowflaking, toSnowflaking_comp_ofSnowflaking, preimage_toSnowflaking_ball, edist_toSnowflaking_toSnowflaking, uniformEquiv_symm_apply, image_toSnowflaking_closedBall, preimage_ofSnowflaking_eball, uniformContinuous_toSnowflaking, image_toSnowflaking_closedEBall, preimage_ofSnowflaking_emetricBall, isBounded_preimage_toSnowflaking_iff, ediam_preimage_toSnowflaking, preimage_ofSnowflaking_emetricClosedBall, homeomorph_symm_apply, image_toSnowflaking_image_ofSnowflaking, image_toSnowflaking_ball, image_ofSnowflaking_image_toSnowflaking, preimage_ofSnowflaking_closedEBall, preimage_toSnowflaking_emetricBall, dist_toSnowflaking_toSnowflaking, image_toSnowflaking_emetricBall, ediam_image_toSnowflaking, isBounded_image_toSnowflaking_iff
uniformEquiv 📖	CompOp	3 math math: uniformEquiv_toEquiv, uniformEquiv_symm_apply, uniformEquiv_apply
val 📖	CompOp	3 math math: val_eq_ofSnowflaking, ext_iff, uniformEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_ofSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Continuous Metric.Snowflaking instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking	—	continuous_induced_dom
continuous_toSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Continuous Metric.Snowflaking instTopologicalSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking	—	continuous_induced_rng continuous_id
dist_ofSnowflaking_ofSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Dist.dist PseudoMetricSpace.toDist DFunLike.coe Equiv Metric.Snowflaking EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking Real.instPow instDist Real.instInv	—	Real.rpow_rpow_inv dist_nonneg LT.lt.ne'
dist_toSnowflaking_toSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Dist.dist Metric.Snowflaking instDist DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking Real.instPow	—	—
ediam_image_ofSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Metric.ediam Set.image Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking ENNReal ENNReal.instPowReal instPseudoEMetricSpace Real.instInv	—	eq_of_forall_ge_iff edist_ofSnowflaking_ofSnowflaking ENNReal.rpow_inv_le_iff
ediam_image_toSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Metric.ediam Metric.Snowflaking instPseudoEMetricSpace Set.image DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking ENNReal ENNReal.instPowReal	—	image_toSnowflaking_eq_preimage ediam_preimage_ofSnowflaking
ediam_preimage_ofSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Metric.ediam Metric.Snowflaking instPseudoEMetricSpace Set.preimage DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking ENNReal ENNReal.instPowReal	—	ENNReal.rpow_inv_rpow LT.lt.ne' ediam_preimage_toSnowflaking Set.preimage_comp ofSnowflaking_comp_toSnowflaking Set.preimage_id
ediam_preimage_toSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Metric.ediam Set.preimage Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking ENNReal ENNReal.instPowReal instPseudoEMetricSpace Real.instInv	—	image_ofSnowflaking_eq_preimage ediam_image_ofSnowflaking
edist_def 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	EDist.edist Metric.Snowflaking instEDist ENNReal ENNReal.instPowReal DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking	—	—
edist_ofSnowflaking_ofSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	EDist.edist DFunLike.coe Equiv Metric.Snowflaking EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking ENNReal ENNReal.instPowReal instEDist Real.instInv	—	edist_def ENNReal.rpow_rpow_inv LT.lt.ne'
edist_toSnowflaking_toSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	EDist.edist Metric.Snowflaking instEDist DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking ENNReal ENNReal.instPowReal	—	—
ext 📖	—	Real Real.instLT Real.instZero Real.instLE Real.instOne val	—	—	—
ext_iff 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	val	—	ext
homeomorph_apply 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	DFunLike.coe Homeomorph Metric.Snowflaking instTopologicalSpace EquivLike.toFunLike Homeomorph.instEquivLike homeomorph Equiv Equiv.instEquivLike ofSnowflaking	—	—
homeomorph_symm_apply 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	DFunLike.coe Homeomorph Metric.Snowflaking instTopologicalSpace EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm homeomorph Equiv Equiv.instEquivLike toSnowflaking	—	—
image_ofSnowflaking_ball 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.image Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking Metric.ball instPseudoMetricSpace Real.instPow Real.instInv	—	image_ofSnowflaking_eq_preimage preimage_toSnowflaking_ball
image_ofSnowflaking_closedBall 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.image Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking Metric.closedBall instPseudoMetricSpace Real.instPow Real.instInv	—	image_ofSnowflaking_eq_preimage preimage_toSnowflaking_closedBall
image_ofSnowflaking_closedEBall 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.image Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking Metric.closedEBall instPseudoEMetricSpace ENNReal ENNReal.instPowReal Real.instInv	—	image_ofSnowflaking_eq_preimage preimage_toSnowflaking_closedEBall
image_ofSnowflaking_eball 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.image Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking Metric.eball instPseudoEMetricSpace ENNReal ENNReal.instPowReal Real.instInv	—	image_ofSnowflaking_eq_preimage preimage_toSnowflaking_eball
image_ofSnowflaking_emetricBall 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.image Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking Metric.eball instPseudoEMetricSpace ENNReal ENNReal.instPowReal Real.instInv	—	image_ofSnowflaking_eball
image_ofSnowflaking_emetricClosedBall 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.image Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking Metric.closedEBall instPseudoEMetricSpace ENNReal ENNReal.instPowReal Real.instInv	—	image_ofSnowflaking_closedEBall
image_ofSnowflaking_eq_preimage 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.image Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking Set.preimage toSnowflaking	—	Equiv.image_eq_preimage_symm
image_ofSnowflaking_image_toSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.image Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking toSnowflaking	—	Equiv.image_symm_image
image_toSnowflaking_ball 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.image Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking Metric.ball instPseudoMetricSpace Real.instPow	—	image_toSnowflaking_eq_preimage preimage_ofSnowflaking_ball
image_toSnowflaking_closedBall 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.image Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking Metric.closedBall instPseudoMetricSpace Real.instPow	—	image_toSnowflaking_eq_preimage preimage_ofSnowflaking_closedBall
image_toSnowflaking_closedEBall 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.image Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking Metric.closedEBall instPseudoEMetricSpace ENNReal ENNReal.instPowReal	—	image_toSnowflaking_eq_preimage preimage_ofSnowflaking_closedEBall
image_toSnowflaking_eball 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.image Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking Metric.eball instPseudoEMetricSpace ENNReal ENNReal.instPowReal	—	image_toSnowflaking_eq_preimage preimage_ofSnowflaking_eball
image_toSnowflaking_emetricBall 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.image Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking Metric.eball instPseudoEMetricSpace ENNReal ENNReal.instPowReal	—	image_toSnowflaking_eball
image_toSnowflaking_emetricClosedBall 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.image Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking Metric.closedEBall instPseudoEMetricSpace ENNReal ENNReal.instPowReal	—	image_toSnowflaking_closedEBall
image_toSnowflaking_eq_preimage 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.image Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking Set.preimage ofSnowflaking	—	Equiv.image_eq_preimage_symm
image_toSnowflaking_image_ofSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.image Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking ofSnowflaking	—	Equiv.symm_image_image
instSecondCountableTopology 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	SecondCountableTopology Metric.Snowflaking instTopologicalSpace	—	Homeomorph.secondCountableTopology
instT0Space 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	T0Space Metric.Snowflaking instTopologicalSpace	—	Homeomorph.t0Space
instT2Space 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	T2Space Metric.Snowflaking instTopologicalSpace	—	Homeomorph.t2Space
isBounded_image_ofSnowflaking_iff 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Bornology.IsBounded Set.image Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking instBornology	—	Bornology.isBounded_induced
isBounded_image_toSnowflaking_iff 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Bornology.IsBounded Metric.Snowflaking instBornology Set.image DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking	—	isBounded_image_ofSnowflaking_iff image_ofSnowflaking_image_toSnowflaking
isBounded_preimage_ofSnowflaking_iff 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Bornology.IsBounded Metric.Snowflaking instBornology Set.preimage DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking	—	image_toSnowflaking_eq_preimage isBounded_image_toSnowflaking_iff
isBounded_preimage_toSnowflaking_iff 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Bornology.IsBounded Set.preimage Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking instBornology	—	image_ofSnowflaking_eq_preimage isBounded_image_ofSnowflaking_iff
mk_eq_toSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	DFunLike.coe Equiv Metric.Snowflaking EquivLike.toFunLike Equiv.instEquivLike toSnowflaking	—	—
ofSnowflaking_comp_toSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking toSnowflaking	—	—
ofSnowflaking_toSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	DFunLike.coe Equiv Metric.Snowflaking EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking toSnowflaking	—	—
preimage_ofSnowflaking_ball 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.preimage Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking Metric.ball instPseudoMetricSpace toSnowflaking Real.instPow	—	Set.ext dist_nonneg
preimage_ofSnowflaking_closedBall 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.preimage Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking Metric.closedBall instPseudoMetricSpace toSnowflaking Real.instPow	—	Set.ext dist_nonneg
preimage_ofSnowflaking_closedEBall 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.preimage Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking Metric.closedEBall instPseudoEMetricSpace toSnowflaking ENNReal ENNReal.instPowReal	—	Set.ext
preimage_ofSnowflaking_eball 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.preimage Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking Metric.eball instPseudoEMetricSpace toSnowflaking ENNReal ENNReal.instPowReal	—	Set.ext
preimage_ofSnowflaking_emetricBall 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.preimage Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking Metric.eball instPseudoEMetricSpace toSnowflaking ENNReal ENNReal.instPowReal	—	preimage_ofSnowflaking_eball
preimage_ofSnowflaking_emetricClosedBall 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.preimage Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking Metric.closedEBall instPseudoEMetricSpace toSnowflaking ENNReal ENNReal.instPowReal	—	preimage_ofSnowflaking_closedEBall
preimage_toSnowflaking_ball 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.preimage Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking Metric.ball instPseudoMetricSpace ofSnowflaking Real.instPow Real.instInv	—	Equiv.preimage_eq_iff_eq_image image_toSnowflaking_ball Real.rpow_nonneg toSnowflaking_ofSnowflaking Real.rpow_inv_rpow LT.lt.ne'
preimage_toSnowflaking_closedBall 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.preimage Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking Metric.closedBall instPseudoMetricSpace ofSnowflaking Real.instPow Real.instInv	—	Equiv.preimage_eq_iff_eq_image image_toSnowflaking_closedBall Real.rpow_nonneg toSnowflaking_ofSnowflaking Real.rpow_inv_rpow LT.lt.ne'
preimage_toSnowflaking_closedEBall 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.preimage Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking Metric.closedEBall instPseudoEMetricSpace ofSnowflaking ENNReal ENNReal.instPowReal Real.instInv	—	Equiv.preimage_eq_iff_eq_image image_toSnowflaking_closedEBall toSnowflaking_ofSnowflaking ENNReal.rpow_inv_rpow LT.lt.ne'
preimage_toSnowflaking_eball 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.preimage Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking Metric.eball instPseudoEMetricSpace ofSnowflaking ENNReal ENNReal.instPowReal Real.instInv	—	Equiv.preimage_eq_iff_eq_image image_toSnowflaking_eball toSnowflaking_ofSnowflaking ENNReal.rpow_inv_rpow LT.lt.ne'
preimage_toSnowflaking_emetricBall 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.preimage Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking Metric.eball instPseudoEMetricSpace ofSnowflaking ENNReal ENNReal.instPowReal Real.instInv	—	preimage_toSnowflaking_eball
preimage_toSnowflaking_emetricClosedBall 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Set.preimage Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking Metric.closedEBall instPseudoEMetricSpace ofSnowflaking ENNReal ENNReal.instPowReal Real.instInv	—	preimage_toSnowflaking_closedEBall
symm_ofSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Equiv.symm Metric.Snowflaking ofSnowflaking toSnowflaking	—	—
symm_toSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Equiv.symm Metric.Snowflaking toSnowflaking ofSnowflaking	—	—
toEquiv_homeomorph 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Homeomorph.toEquiv Metric.Snowflaking instTopologicalSpace homeomorph ofSnowflaking	—	—
toSnowflaking_comp_ofSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking ofSnowflaking	—	—
toSnowflaking_ofSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	DFunLike.coe Equiv Metric.Snowflaking EquivLike.toFunLike Equiv.instEquivLike toSnowflaking ofSnowflaking	—	—
uniformContinuous_ofSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	UniformContinuous Metric.Snowflaking instUniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking	—	uniformContinuous_comap
uniformContinuous_toSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	UniformContinuous Metric.Snowflaking instUniformSpace DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike toSnowflaking	—	uniformContinuous_comap' uniformContinuous_id
uniformEquiv_apply 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	DFunLike.coe UniformEquiv Metric.Snowflaking instUniformSpace EquivLike.toFunLike UniformEquiv.instEquivLike uniformEquiv val	—	—
uniformEquiv_symm_apply 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	DFunLike.coe UniformEquiv Metric.Snowflaking instUniformSpace EquivLike.toFunLike UniformEquiv.instEquivLike UniformEquiv.symm uniformEquiv Equiv Equiv.instEquivLike toSnowflaking	—	—
uniformEquiv_toEquiv 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	UniformEquiv.toEquiv Metric.Snowflaking instUniformSpace uniformEquiv ofSnowflaking	—	—
val_eq_ofSnowflaking 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	val DFunLike.coe Equiv Metric.Snowflaking EquivLike.toFunLike Equiv.instEquivLike ofSnowflaking	—	—

Metric.Snowflaking.toSnowflaking

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sizeOf_spec 📖	mathematical	Real Real.instLT Real.instZero Real.instLE Real.instOne	Metric.Snowflaking DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Metric.Snowflaking.toSnowflaking	—	—

---

← Back to Index