Documentation Verification Report

Tietze

📁 Source: Mathlib/Analysis/Complex/Tietze.lean

Statistics

Metric	Count
Definitions	0
Theorems `exists_norm_eq_restrict_eq`, `instTietzeExtension`, `instTietzeExtensionBall`, `instTietzeExtensionClosedBall`, `instTietzeExtension`, `instTietzeExtensionTVS`, `instTietzeExtensionUnitBall`, `instTietzeExtensionUnitClosedBall`, `of_tvs`, `instTietzeExtension`	10
Total	10

BoundedContinuousFunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_norm_eq_restrict_eq` 📖	mathematical	—	`Norm.norm` `BoundedContinuousFunction` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instNorm` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `restrict`	—	`norm_zero` `Metric.instTietzeExtensionClosedBall` `dist_zero_right` `norm_coe_le_norm` `BoundedContinuousMapClass.toContinuousMapClass` `instBoundedContinuousMapClass` `ContinuousMap.exists_forall_mem_restrict_eq` `ContinuousMapClass.map_continuous` `ContinuousMap.instContinuousMapClass` `le_antisymm` `norm_le` `le_of_lt` `lt_of_le_of_ne'` `norm_nonneg` `le_rfl` `ext`

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instTietzeExtension` 📖	mathematical	—	`TietzeExtension` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField`	—	`TietzeExtension.of_tvs` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `instT2Space` `FiniteDimensional.rclike_to_real` `Real.instCompleteSpace` `Real.instTietzeExtension`

Metric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instTietzeExtensionBall` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`TietzeExtension` `Set.Elem` `ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`TietzeExtension.of_homeo` `Set.instTietzeExtensionUnitBall`
`instTietzeExtensionClosedBall` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`TietzeExtension` `Set.Elem` `closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`TietzeExtension.of_homeo` `Set.instTietzeExtensionUnitClosedBall` `NormedSpace.toNormSMulClass` `Nat.cast_zero` `algebraMap.coe_zero` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `LT.lt.ne'` `Set.ext` `dist_zero_right` `dist_add_self_left` `norm_smul` `RCLike.norm_ofReal` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `LT.lt.le` `mul_le_iff_le_one_right` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing`

RCLike

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instTietzeExtension` 📖	mathematical	—	`TietzeExtension` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `toDenselyNormedField`	—	`TietzeExtension.of_tvs` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `FiniteDimensional.rclike_to_real` `Real.instCompleteSpace` `Real.instTietzeExtension`
`instTietzeExtensionTVS` 📖	mathematical	—	`TietzeExtension`	—	`TietzeExtension.of_tvs` `toCompleteSpace` `instTietzeExtension`

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instTietzeExtensionUnitBall` 📖	mathematical	—	`TietzeExtension` `Elem` `Metric.ball` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne` `instTopologicalSpaceSubtype` `Set` `instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`TietzeExtension.of_homeo` `RCLike.instTietzeExtensionTVS` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`instTietzeExtensionUnitClosedBall` 📖	mathematical	—	`TietzeExtension` `Elem` `Metric.closedBall` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real` `Real.instOne` `instTopologicalSpaceSubtype` `Set` `instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace`	—	`Real.isScalarTower` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `continuous_piecewise` `frontier_closedBall` `one_ne_zero` `NeZero.charZero_one` `RCLike.charZero_rclike` `sub_zero` `inv_one` `one_smul` `continuousOn_id` `ContinuousOn.smul` `ContinuousOn.inv₀` `IsTopologicalDivisionRing.toContinuousInv₀` `instIsTopologicalDivisionRingReal` `ContinuousOn.norm` `closure_compl` `interior_closedBall` `dist_zero_right` `norm_pos_iff` `LT.lt.trans_le` `one_pos` `Real.instZeroLEOneClass` `TietzeExtension.of_retract` `RCLike.instTietzeExtensionTVS` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `continuous_subtype_val` `piecewise_eq_of_mem` `piecewise.congr_simp` `RCLike.real_smul_eq_coe_smul` `piecewise_eq_of_notMem` `norm_zero` `inv_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `smul_zero` `dist_self` `map_inv₀` `norm_smul_inv_norm` `Continuous.codRestrict` `ContinuousMap.ext`

TietzeExtension

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_tvs` 📖	mathematical	—	`TietzeExtension`	—	`of_homeo` `Pi.instTietzeExtension` `RingHomInvPair.ids` `Pi.topologicalAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instContinuousSMulForall` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Pi.t2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Finite.of_fintype` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule`

unitInterval

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instTietzeExtension` 📖	mathematical	—	`TietzeExtension` `Set.Elem` `Real` `unitInterval` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	—	`Nat.instAtLeastTwoHAddOfNat` `eq_closedBall` `Metric.instTietzeExtensionClosedBall` `FiniteDimensional.rclike_to_real` `Mathlib.Meta.NormNum.isNNRat_lt_true` `Real.instIsStrictOrderedRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.instAtLeastTwo`

---

← Back to Index