Documentation Verification Report

TietzeExtension

📁 Source: Mathlib/Topology/TietzeExtension.lean

Statistics

Metric	Count
Definitions `TietzeExtension`	1
Theorems `exists_extension_forall_exists_le_ge_of_isClosedEmbedding`, `exists_extension_forall_mem_Icc_of_isClosedEmbedding`, `exists_extension_forall_mem_of_isClosedEmbedding`, `exists_extension_norm_eq_of_isClosedEmbedding`, `exists_extension_norm_eq_of_isClosedEmbedding'`, `exists_forall_mem_restrict_eq_of_closed`, `exists_norm_eq_restrict_eq_of_closed`, `tietze_extension_step`, `exists_extension`, `exists_extension'`, `exists_extension_forall_mem`, `exists_extension_forall_mem_of_isClosedEmbedding`, `exists_forall_mem_restrict_eq`, `exists_restrict_eq`, `exists_restrict_eq_forall_mem_of_closed`, `instTietzeExtension`, `instTietzeExtension`, `instTietzeExtension`, `instTietzeExtension`, `exists_restrict_eq'`, `of_homeo`, `of_retract`, `instTietzeExtension`	23
Total	24

BoundedContinuousFunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_extension_forall_exists_le_ge_of_isClosedEmbedding` 📖	mathematical	`Topology.IsClosedEmbedding`	`Real` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder` `DFunLike.coe` `BoundedContinuousFunction` `Real.pseudoMetricSpace` `instFunLike`	—	`isGLB_ciInf` `Bornology.IsBounded.bddBelow` `Real.instIsOrderBornology` `isBounded_range` `isLUB_ciSup` `Bornology.IsBounded.bddAbove` `LE.le.trans` `LE.le.eq_or_lt` `Set.Icc_self` `Nat.instAtLeastTwoHAddOfNat` `left_lt_add_div_two` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `add_div_two_lt_right` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsRat.to_raw_eq` `Mathlib.Meta.NormNum.isRat_add` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Meta.NormNum.IsInt.to_isRat` `Mathlib.Meta.NormNum.isRat_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.IsRat.of_raw` `Mathlib.Meta.NormNum.IsRat.den_nz` `exists_extension_forall_mem_Icc_of_isClosedEmbedding` `em` `Set.disjoint_union_left` `Set.disjoint_left` `Disjoint.preimage` `Set.disjoint_singleton_right` `LT.lt.not_ge` `exists_bounded_mem_Icc_of_closed_of_le` `IsClosed.union` `Topology.IsClosedEmbedding.isClosed_range` `IsClosed.preimage` `continuous` `isClosed_Ici` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `isClosed_singleton` `T5Space.toT1Space` `OrderTopology.t5Space` `instOrderTopologyReal` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `LT.lt.le` `instBoundedAddOfLipschitzAdd` `Real.hasLipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Set.mem_range_self` `add_zero` `lt_add_iff_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `LT.lt.trans_le` `le_add_of_nonneg_right` `IsGLB.exists_between` `le_total` `add_le_add` `add_sub_cancel` `isClosed_Iic` `instClosedIicTopology` `instBoundedSub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `sub_zero` `sub_lt_self_iff` `LE.le.trans_lt` `sub_le_self_iff` `IsLUB.exists_between` `lt_or_ge` `sub_sub_cancel` `sub_le_sub` `sub_lt_sub_right` `sub_le_sub_left`
`exists_extension_forall_mem_Icc_of_isClosedEmbedding` 📖	—	`Real` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder` `DFunLike.coe` `BoundedContinuousFunction` `Real.pseudoMetricSpace` `instFunLike` `Real.instLE` `Topology.IsClosedEmbedding`	—	—	`instBoundedSub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `Nat.instAtLeastTwoHAddOfNat` `exists_extension_norm_eq_of_isClosedEmbedding` `instBoundedAddOfLipschitzAdd` `Real.hasLipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `norm_le` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `sub_nonneg` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `zero_le_two` `Real.instZeroLEOneClass` `Real.Icc_eq_closedBall` `dist_self_add_left` `LE.le.trans` `norm_coe_le_norm` `Eq.trans_le` `add_sub_cancel`
`exists_extension_forall_mem_of_isClosedEmbedding` 📖	—	`Real` `Set` `Set.instMembership` `DFunLike.coe` `BoundedContinuousFunction` `Real.pseudoMetricSpace` `instFunLike` `Set.Nonempty` `Topology.IsClosedEmbedding`	—	—	`isEmpty_or_nonempty` `exists_extension_forall_exists_le_ge_of_isClosedEmbedding` `Set.OrdConnected.out`
`exists_extension_norm_eq_of_isClosedEmbedding` 📖	mathematical	`Topology.IsClosedEmbedding`	`Norm.norm` `BoundedContinuousFunction` `Real` `Real.pseudoMetricSpace` `instNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `DFunLike.coe` `instFunLike`	—	`Topology.IsClosedEmbedding.continuous` `exists_extension_norm_eq_of_isClosedEmbedding'`
`exists_extension_norm_eq_of_isClosedEmbedding'` 📖	mathematical	`Topology.IsClosedEmbedding` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike`	`Norm.norm` `BoundedContinuousFunction` `Real` `Real.pseudoMetricSpace` `instNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `compContinuous`	—	`Nat.instAtLeastTwoHAddOfNat` `instBoundedAddOfLipschitzAdd` `Real.hasLipschitzAdd` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instBoundedSub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `Function.iterate_succ_apply'` `dist_zero` `pow_zero` `one_mul` `add_compContinuous` `dist_sub_right` `NormedAddGroup.to_isIsometricVAdd_right` `add_sub_cancel_left` `pow_succ'` `mul_assoc` `LE.le.trans` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `dist_eq_norm'` `Mathlib.Meta.NormNum.isRat_le_true` `Real.instIsStrictOrderedRing` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `IsStrictOrderedRing.toCharZero` `one_div` `div_eq_inv_mul` `Nat.cast_one` `Semigroup.to_isAssociative` `CommMagma.to_isCommutative` `cauchySeq_of_le_geometric` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instNontrivialOfCharZero` `Filter.Tendsto.comp` `Continuous.tendsto` `continuous_compContinuous` `CauchySeq.tendsto_limUnder` `instCompleteSpace` `Real.instCompleteSpace` `tendsto_nhds_unique` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `tendsto_iff_dist_tendsto_zero` `squeeze_zero` `dist_nonneg` `MulZeroClass.zero_mul` `Filter.Tendsto.mul` `IsTopologicalSemiring.toContinuousMul` `tendsto_pow_atTop_nhds_zero_of_lt_one` `AddGroup.existsAddOfLE` `Real.instArchimedean` `instOrderTopologyReal` `tendsto_const_nhds` `le_antisymm` `dist_zero_left` `LE.le.trans_eq` `Filter.NeBot.nonempty` `dist_le_of_le_geometric_of_tendsto₀` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.div_pf` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsRat.to_raw_eq` `Mathlib.Meta.NormNum.isRat_mul` `Mathlib.Meta.NormNum.IsInt.to_isRat` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_add` `Mathlib.Meta.NormNum.IsRat.of_raw` `Mathlib.Meta.NormNum.IsRat.den_nz` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Tactic.Ring.mul_pf_left` `norm_compContinuous_le` `tietze_extension_step`
`exists_forall_mem_restrict_eq_of_closed` 📖	mathematical	`Real` `Set` `Set.instMembership` `DFunLike.coe` `BoundedContinuousFunction` `Set.Elem` `instTopologicalSpaceSubtype` `Real.pseudoMetricSpace` `instFunLike` `Set.Nonempty`	`restrict`	—	`exists_extension_forall_mem_of_isClosedEmbedding` `IsClosed.isClosedEmbedding_subtypeVal` `DFunLike.coe_injective`
`exists_norm_eq_restrict_eq_of_closed` 📖	mathematical	—	`Norm.norm` `BoundedContinuousFunction` `Real` `Real.pseudoMetricSpace` `instNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `restrict`	—	`exists_extension_norm_eq_of_isClosedEmbedding'` `IsClosed.isClosedEmbedding_subtypeVal`
`tietze_extension_step` 📖	mathematical	`Topology.IsClosedEmbedding` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike`	`Real` `Real.instLE` `Norm.norm` `BoundedContinuousFunction` `Real.pseudoMetricSpace` `instNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Dist.dist` `instDist` `compContinuous` `Real.instMul`	—	`Nat.instAtLeastTwoHAddOfNat` `Mathlib.Meta.NormNum.isNat_lt_true` `Real.instIsOrderedRing` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instNontrivialOfCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `eq_or_ne` `norm_zero` `zero_div` `dist_zero_right` `MulZeroClass.mul_zero` `norm_pos_iff` `div_lt_div_iff_of_pos_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Left.neg_lt_self` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Topology.IsClosedEmbedding.isClosedMap` `IsClosed.preimage` `continuous` `isClosed_Iic` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `isClosed_Ici` `instClosedIciTopology` `Set.disjoint_image_of_injective` `Topology.IsEmbedding.injective` `Topology.IsClosedEmbedding.toIsEmbedding` `Disjoint.preimage` `Set.Iic_disjoint_Ici` `not_le` `exists_bounded_mem_Icc_of_closed_of_le` `LT.lt.le` `norm_le` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `neg_div` `dist_le` `mul_nonneg` `IsOrderedRing.toPosMulMono` `norm_coe_le_norm` `le_total` `Set.mem_image_of_mem` `abs_of_nonneg` `sub_nonneg` `covariant_swap_add_of_covariant_add` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Nat.cast_one` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `CancelDenoms.derive_trans` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `CancelDenoms.sub_subst` `CancelDenoms.mul_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNat_mul` `CancelDenoms.neg_subst` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `dist_le_norm_add_norm` `add_le_add` `abs_le` `Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt` `CancelDenoms.add_subst` `abs_sub_comm` `Mathlib.Tactic.Ring.add_pf_add_gt`

ContinuousMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_extension` 📖	mathematical	`Topology.IsClosedEmbedding`	`comp` `Topology.IsClosedEmbedding.continuous`	—	`Topology.IsClosedEmbedding.isEmbedding` `Homeomorph.instContinuousMapClass` `Topology.IsClosedEmbedding.continuous` `exists_restrict_eq` `Topology.IsClosedEmbedding.isClosed_range` `ext` `Subtype.coe_eta` `Homeomorph.symm_apply_apply`
`exists_extension'` 📖	mathematical	`Topology.IsClosedEmbedding`	`DFunLike.coe` `ContinuousMap` `instFunLike`	—	`Topology.IsClosedEmbedding.continuous` `exists_extension`
`exists_extension_forall_mem` 📖	mathematical	`Topology.IsClosedEmbedding` `Set` `Set.instMembership` `DFunLike.coe` `ContinuousMap` `instFunLike`	`comp` `Topology.IsClosedEmbedding.continuous`	—	`Topology.IsClosedEmbedding.continuous` `Continuous.codRestrict` `ContinuousMapClass.map_continuous` `instContinuousMapClass` `exists_extension` `continuous_subtype_val` `ext`
`exists_extension_forall_mem_of_isClosedEmbedding` 📖	—	`Real` `Set` `Set.instMembership` `DFunLike.coe` `ContinuousMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instFunLike` `Set.Nonempty` `Topology.IsClosedEmbedding`	—	—	`Real.instIsStrictOrderedRing` `Continuous.comp'` `continuous_subtype_val` `ContinuousMapClass.map_continuous` `HomeomorphClass.instContinuousMapClass` `OrderIso.instHomeomorphClass` `instOrderTopologyReal` `orderTopology_of_ordConnected` `Set.ordConnected_Ioo` `instContinuousMapClass` `Metric.isBounded_range_iff` `Bornology.IsBounded.subset` `Metric.isBounded_Ioo` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `Set.range_subset_iff` `Set.image_subset_iff` `CanLift.prf` `Subtype.canLift` `Set.Icc_subset_Ioo` `OrderIso.image_Icc` `Set.OrdConnected.out` `Set.mem_image_of_mem` `BoundedContinuousFunction.exists_extension_forall_mem_of_isClosedEmbedding` `Set.Nonempty.image` `Continuous.comp` `OrderIso.continuous` `BoundedContinuousFunction.continuous` `Equiv.symm_apply_eq`
`exists_forall_mem_restrict_eq` 📖	mathematical	`Set` `Set.instMembership` `DFunLike.coe` `ContinuousMap` `Set.Elem` `instTopologicalSpaceSubtype` `instFunLike`	`restrict`	—	`Continuous.codRestrict` `ContinuousMapClass.map_continuous` `instContinuousMapClass` `exists_restrict_eq` `continuous_subtype_val` `ext`
`exists_restrict_eq` 📖	mathematical	—	`restrict`	—	`TietzeExtension.exists_restrict_eq'`
`exists_restrict_eq_forall_mem_of_closed` 📖	mathematical	`Real` `Set` `Set.instMembership` `DFunLike.coe` `ContinuousMap` `Set.Elem` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `instFunLike` `Set.Nonempty`	`restrict`	—	`exists_extension_forall_mem_of_isClosedEmbedding` `IsClosed.isClosedEmbedding_subtypeVal` `coe_injective`

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instTietzeExtension` 📖	mathematical	—	`TietzeExtension` `NNReal` `instTopologicalSpace`	—	`TietzeExtension.of_retract` `Real.instTietzeExtension` `continuous_induced_dom` `continuous_real_toNNReal` `ContinuousMap.ext` `eq` `Real.toNNReal_coe`

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instTietzeExtension` 📖	mathematical	`TietzeExtension`	`topologicalSpace`	—	`ContinuousMap.exists_restrict_eq` `ContinuousMap.ext`

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instTietzeExtension` 📖	mathematical	—	`TietzeExtension` `instTopologicalSpaceProd`	—	`ContinuousMap.exists_restrict_eq` `ContinuousMap.ext`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instTietzeExtension` 📖	mathematical	—	`TietzeExtension` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace`	—	`ContinuousMap.exists_restrict_eq_forall_mem_of_closed` `Set.ordConnected_univ` `Set.mem_univ` `Set.univ_nonempty`

TietzeExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_restrict_eq'` 📖	mathematical	—	`ContinuousMap.restrict`	—	—
`of_homeo` 📖	mathematical	—	`TietzeExtension`	—	`of_retract` `Homeomorph.instContinuousMapClass` `Homeomorph.symm_comp_toContinuousMap`
`of_retract` 📖	mathematical	`ContinuousMap.comp` `ContinuousMap.id`	`TietzeExtension`	—	`ContinuousMap.exists_restrict_eq` `ContinuousMap.ext` `ContinuousMap.id_comp` `ContinuousMap.comp_assoc`

Unique

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instTietzeExtension` 📖	mathematical	—	`TietzeExtension`	—	`ContinuousMap.ext`

(root)

Definitions

Name	Category	Theorems
`TietzeExtension` 📖	CompData	15 math math: `Set.instTietzeExtensionUnitBall`, `NNReal.instTietzeExtension`, `Prod.instTietzeExtension`, `unitInterval.instTietzeExtension`, `TietzeExtension.of_retract`, `Set.instTietzeExtensionUnitClosedBall`, `Complex.instTietzeExtension`, `Unique.instTietzeExtension`, `Metric.instTietzeExtensionClosedBall`, `TietzeExtension.of_homeo`, `Metric.instTietzeExtensionBall`, `RCLike.instTietzeExtension`, `RCLike.instTietzeExtensionTVS`, `TietzeExtension.of_tvs`, `Real.instTietzeExtension`

---

← Back to Index