Antilipschitz

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

Statistics

Metric	Count
Definitions `AntilipschitzWith`, `k`	2
Theorems `codRestrict`, `comap_nhds_le`, `comap_uniformity_le`, `comp`, `ediam_preimage_le`, `edist_lt_top`, `edist_ne_top`, `id`, `injective`, `isBounded_of_image2_left`, `isBounded_of_image2_right`, `isBounded_preimage`, `isClosedEmbedding`, `isClosed_range`, `isComplete_range`, `isEmbedding`, `isInducing`, `isUniformEmbedding`, `isUniformInducing`, `le_mul_dist`, `le_mul_ediam_image`, `le_mul_nndist`, `mul_le_dist`, `mul_le_edist`, `mul_le_nndist`, `of_le_mul_dist`, `of_le_mul_nndist`, `of_subsingleton`, `properSpace`, `restrict`, `subsingleton`, `subtype_coe`, `tendsto_cobounded`, `to_rightInvOn`, `to_rightInvOn'`, `to_rightInverse`, `to_rightInverse`, `antilipschitzWith_iff_le_mul_dist`, `antilipschitzWith_iff_le_mul_nndist`	39
Total	41

AntilipschitzWith

Definitions

Name	Category	Theorems
`k` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`codRestrict` 📖	mathematical	`AntilipschitzWith` `Set` `Set.instMembership`	`Set.Elem` `instPseudoEMetricSpaceSubtype` `Set.codRestrict`	—	—
`comap_nhds_le` 📖	mathematical	`AntilipschitzWith`	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.comap` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	—	`nhds_eq_comap_uniformity` `le_imp_le_of_le_of_le` `le_refl` `Filter.comap_mono` `comap_uniformity_le` `Filter.comap_comap`
`comap_uniformity_le` 📖	mathematical	`AntilipschitzWith`	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.comap` `uniformity` `PseudoEMetricSpace.toUniformSpace`	—	`Filter.HasBasis.le_basis_iff` `Filter.HasBasis.comap` `uniformity_basis_edist` `ENNReal.mul_pos` `ENNReal.inv_ne_zero` `ENNReal.coe_ne_top` `LT.lt.ne'` `LE.le.trans_lt` `mul_comm` `ENNReal.mul_lt_of_lt_div` `div_eq_mul_inv`
`comp` 📖	mathematical	`AntilipschitzWith`	`NNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`mul_right_mono` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `ENNReal.coe_mul` `mul_assoc`
`ediam_preimage_le` 📖	mathematical	`AntilipschitzWith`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam` `Set.preimage` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	—	`Metric.ediam_le` `le_imp_le_of_le_of_le` `le_refl` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `Metric.edist_le_ediam_of_mem` `Set.mem_preimage`
`edist_lt_top` 📖	mathematical	`AntilipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `EDist.edist` `PseudoEMetricSpace.toEDist` `Top.top` `instTopENNReal`	—	`LE.le.trans_lt` `ENNReal.mul_lt_top` `ENNReal.coe_lt_top` `edist_lt_top`
`edist_ne_top` 📖	—	`AntilipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	—	—	`LT.lt.ne` `edist_lt_top`
`id` 📖	mathematical	—	`AntilipschitzWith` `NNReal` `instOneNNReal`	—	`one_mul`
`injective` 📖	—	`AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace`	—	—	`PseudoEMetricSpace.edist_self` `MulZeroClass.mul_zero`
`isBounded_of_image2_left` 📖	—	`AntilipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `Bornology.IsBounded` `PseudoMetricSpace.toBornology` `Set.image2`	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Bornology.nonempty_of_not_isBounded` `isBounded_preimage` `Set.image2_singleton_right` `Bornology.IsBounded.subset` `Set.subset_preimage_image` `Set.image2_subset` `subset_rfl` `Set.instReflSubset` `Set.singleton_subset_iff`
`isBounded_of_image2_right` 📖	—	`AntilipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `Bornology.IsBounded` `PseudoMetricSpace.toBornology` `Set.image2`	—	—	`isBounded_of_image2_left` `Set.image2_swap`
`isBounded_preimage` 📖	mathematical	`AntilipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `Bornology.IsBounded` `PseudoMetricSpace.toBornology`	`Set.preimage`	—	`Metric.isBounded_iff_ediam_ne_top` `ne_top_of_le_ne_top` `ENNReal.mul_ne_top` `ENNReal.coe_ne_top` `Bornology.IsBounded.ediam_ne_top` `ediam_preimage_le`
`isClosedEmbedding` 📖	mathematical	`AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `UniformContinuous` `PseudoEMetricSpace.toUniformSpace`	`Topology.IsClosedEmbedding` `UniformSpace.toTopologicalSpace`	—	`IsUniformEmbedding.isEmbedding` `isUniformEmbedding` `isClosed_range`
`isClosed_range` 📖	mathematical	`AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `UniformContinuous` `PseudoEMetricSpace.toUniformSpace`	`IsClosed` `UniformSpace.toTopologicalSpace` `Set.range`	—	`IsComplete.isClosed` `EMetricSpace.instT0Space` `isComplete_range`
`isComplete_range` 📖	mathematical	`AntilipschitzWith` `UniformContinuous` `PseudoEMetricSpace.toUniformSpace`	`IsComplete` `Set.range`	—	`IsUniformInducing.isComplete_range` `isUniformInducing`
`isEmbedding` 📖	mathematical	`AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `Continuous` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`Topology.IsEmbedding`	—	`Topology.IsInducing.isEmbedding` `EMetricSpace.instT0Space` `isInducing`
`isInducing` 📖	mathematical	`AntilipschitzWith` `Continuous` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace`	`Topology.IsInducing`	—	`Topology.isInducing_iff_nhds` `le_antisymm` `Filter.Tendsto.le_comap` `Continuous.tendsto` `comap_nhds_le`
`isUniformEmbedding` 📖	mathematical	`AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `UniformContinuous` `PseudoEMetricSpace.toUniformSpace`	`IsUniformEmbedding`	—	`isUniformInducing` `injective`
`isUniformInducing` 📖	mathematical	`AntilipschitzWith` `UniformContinuous` `PseudoEMetricSpace.toUniformSpace`	`IsUniformInducing`	—	`le_antisymm` `comap_uniformity_le` `Filter.Tendsto.le_comap`
`le_mul_dist` 📖	mathematical	`AntilipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `NNReal.toReal`	—	`antilipschitzWith_iff_le_mul_dist`
`le_mul_ediam_image` 📖	mathematical	`AntilipschitzWith`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Metric.ediam` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal` `Set.image`	—	`LE.le.trans` `Metric.ediam_mono` `Set.subset_preimage_image` `ediam_preimage_le`
`le_mul_nndist` 📖	mathematical	`AntilipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`antilipschitzWith_iff_le_mul_nndist`
`mul_le_dist` 📖	mathematical	`AntilipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`Real` `Real.instLE` `Real.instMul` `NNReal.toReal` `NNReal` `NNReal.instInv` `Dist.dist` `PseudoMetricSpace.toDist`	—	`mul_le_nndist`
`mul_le_edist` 📖	mathematical	`AntilipschitzWith`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instInv` `ENNReal.ofNNReal` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`mul_comm` `div_eq_mul_inv` `ENNReal.div_le_of_le_mul'`
`mul_le_nndist` 📖	mathematical	`AntilipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal` `NNReal.instInv` `NNDist.nndist` `PseudoMetricSpace.toNNDist`	—	`div_eq_inv_mul` `NNReal.div_le_of_le_mul'` `le_mul_nndist`
`of_le_mul_dist` 📖	mathematical	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `NNReal.toReal`	`AntilipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`antilipschitzWith_iff_le_mul_dist`
`of_le_mul_nndist` 📖	mathematical	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	`AntilipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`antilipschitzWith_iff_le_mul_nndist`
`of_subsingleton` 📖	mathematical	—	`AntilipschitzWith`	—	`PseudoEMetricSpace.edist_self` `ENNReal.instCanonicallyOrderedAdd`
`properSpace` 📖	mathematical	`AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `PseudoMetricSpace.toPseudoEMetricSpace` `Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace`	`ProperSpace`	—	`IsClosed.preimage` `Metric.isClosed_closedBall` `isBounded_preimage` `Metric.isBounded_closedBall` `Metric.isCompact_iff_isClosed_bounded` `TopologicalSpace.t2Space_of_metrizableSpace` `TopologicalSpace.PseudoMetrizableSpace.toMetrizableSpace` `MetricSpace.instT0Space` `UniformSpace.pseudoMetrizableSpace` `EMetric.instIsCountablyGeneratedUniformity` `Function.Surjective.image_preimage` `IsCompact.image`
`restrict` 📖	mathematical	`AntilipschitzWith`	`Set.Elem` `instPseudoEMetricSpaceSubtype` `Set` `Set.instMembership` `Set.restrict`	—	—
`subsingleton` 📖	—	`AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace` `NNReal` `instZeroNNReal`	—	—	`edist_le_zero` `LE.le.trans_eq` `MulZeroClass.zero_mul`
`subtype_coe` 📖	mathematical	—	`AntilipschitzWith` `Set` `Set.instMembership` `instPseudoEMetricSpaceSubtype` `NNReal` `instOneNNReal`	—	`restrict` `id`
`tendsto_cobounded` 📖	mathematical	`AntilipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	`Filter.Tendsto` `Bornology.cobounded` `PseudoMetricSpace.toBornology`	—	`Function.Surjective.forall` `compl_surjective` `isBounded_preimage`
`to_rightInvOn` 📖	mathematical	`AntilipschitzWith` `Set.RightInvOn`	`LipschitzWith` `Set.Elem` `instPseudoEMetricSpaceSubtype` `Set` `Set.instMembership` `Set.restrict`	—	`to_rightInvOn'` `restrict` `Set.mapsTo_univ`
`to_rightInvOn'` 📖	mathematical	`AntilipschitzWith` `Set.Elem` `instPseudoEMetricSpaceSubtype` `Set` `Set.instMembership` `Set.restrict` `Set.MapsTo` `Set.RightInvOn`	`LipschitzWith`	—	`Subtype.mem`
`to_rightInverse` 📖	mathematical	`AntilipschitzWith`	`LipschitzWith`	—	—

LipschitzWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`to_rightInverse` 📖	mathematical	`LipschitzWith`	`AntilipschitzWith`	—	—

(root)

Definitions

Name	Category	Theorems
`AntilipschitzWith` 📖	MathDef	45 math math: `ContinuousLinearEquiv.antilipschitz`, `LinearIsometryEquiv.antilipschitz`, `AntilipschitzWith.of_subsingleton`, `IsometryClass.antilipschitz`, `AntilipschitzWith.id`, `Dilation.antilipschitz`, `AntilipschitzWith.of_le_mul_dist`, `antilipschitzWith_iff_le_mul_dist`, `ContinuousLinearMap.antilipschitz_of_isEmbedding`, `PiLp.antilipschitzWith_toLp`, `antilipschitzWith_iff_exists_mul_le_norm'`, `antilipschitzWith_mul_right`, `LinearMap.exists_antilipschitzWith`, `antilipschitzWith_iff_le_mul_nndist`, `Complex.antilipschitz_equivRealProd`, `AddMonoidHomClass.antilipschitz_of_bound`, `WithLp.prod_antilipschitzWith_toLp`, `ContinuousLinearMap.isClosed_range_iff_antilipschitz_of_injective`, `SemilinearIsometryClass.antilipschitz`, `ApproximatesLinearOn.antilipschitz`, `PiLp.antilipschitzWith_ofLp`, `ContinuousLinearMap.antilipschitz_of_injective_of_isClosed_range`, `AntilipschitzWith.subtype_coe`, `MonoidHomClass.antilipschitz_of_bound`, `LipschitzWith.to_rightInverse`, `LinearIsometry.antilipschitz`, `antilipschitzWith_mul_left`, `ContinuousLinearMap.antilipschitz_of_bound`, `Isometry.antilipschitz`, `Unitization.antilipschitzWith_addEquiv`, `antilipschitzWith_inv_iff`, `AffineIsometryEquiv.antilipschitz`, `LinearMap.antilipschitz_of_comap_nhds_le`, `AffineIsometry.antilipschitz`, `antilipschitzWith_neg_iff`, `AffineMap.antilipschitzWith_of_finiteDimensional`, `antilipschitzWith_lineMap`, `LinearMap.injective_iff_antilipschitz`, `ContinuousLinearMap.bijective_iff_dense_range_and_antilipschitz`, `NormedAddGroupHom.antilipschitz_of_norm_ge`, `antilipschitzWith_iff_exists_mul_le_norm`, `ContinuousLinearMap.antilipschitz_of_forall_le_inner_map`, `AntilipschitzWith.of_le_mul_nndist`, `WithLp.prod_antilipschitzWith_ofLp`, `IsCoercive.antilipschitz`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antilipschitzWith_iff_le_mul_dist` 📖	mathematical	—	`AntilipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMul` `NNReal.toReal`	—	—
`antilipschitzWith_iff_le_mul_nndist` 📖	mathematical	—	`AntilipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNDist.nndist` `PseudoMetricSpace.toNNDist` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instSemiringNNReal`	—	`edist_nndist`

---

← Back to Index