Documentation Verification Report

CoveringMap

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

Statistics

Metric	Count
Definitions	0
Theorems `isAddQuotientCoveringMap_exp`, `isCoveringMapOn_exp`, `isCoveringMap_exp`, `isQuotientCoveringMap_npow`, `isCoveringMapOn_eval`, `isCoveringMapOn_npow`, `isCoveringMapOn_zpow`, `isCoveringMap_npow`, `isCoveringMap_zpow`, `isQuotientCoveringMap_npow`, `isQuotientCoveringMap_zpow`	11
Total	11

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddQuotientCoveringMap_exp` 📖	mathematical	—	`IsAddQuotientCoveringMap` `Complex` `instZero` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instTopologicalSpaceSubtype` `exp` `exp_ne_zero` `AddSubgroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `instNormedAddCommGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples` `instMul` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `ofReal` `Real.pi` `I` `AddSubgroup.toAddGroup` `AddAction.instAddAction` `AddTorsor.toAddAction` `NormedAddTorsor.toAddTorsor` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toNormedAddTorsor`	—	`Topology.IsQuotientMap.isAddQuotientCoveringMap_of_addSubgroup` `exp_ne_zero` `IsOpenMap.isQuotientMap` `Topology.IsOpenEmbedding.isOpenMap_iff` `IsOpen.isOpenEmbedding_subtypeVal` `IsClosed.isOpen_compl` `isClosed_singleton` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `isOpenMap_exp` `Continuous.cexp` `continuous_id'` `exp_log` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Nat.instAtLeastTwoHAddOfNat` `NormedSpace.discreteTopology_zmultiples` `instCharZero` `add_comm` `zsmul_eq_mul`
`isCoveringMapOn_exp` 📖	mathematical	—	`IsCoveringMapOn` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `exp` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `instZero`	—	`IsCoveringMapOn.of_isCoveringMap_subtype` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `exp_ne_zero` `isCoveringMap_exp`
`isCoveringMap_exp` 📖	mathematical	—	`IsCoveringMap` `Complex` `instZero` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `instTopologicalSpaceSubtype` `exp` `exp_ne_zero`	—	`IsAddQuotientCoveringMap.isCoveringMap` `exp_ne_zero` `Nat.instAtLeastTwoHAddOfNat` `isAddQuotientCoveringMap_exp`
`isQuotientCoveringMap_npow` 📖	mathematical	—	`IsQuotientCoveringMap` `Units` `Complex` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instSemiring` `Units.instTopologicalSpaceUnits` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `instNormedField` `Monoid.toNatPow` `Units.instMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.ker` `Units.instMulOneClass` `powMonoidHom` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `CommRing.toCommMonoid` `commRing` `Subgroup.toGroup` `MulAction.instMulAction` `Monoid.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`isQuotientCoveringMap_npow` `instProperSpace` `NeZero.charZero` `instCharZero` `cpow_nat_inv_pow`

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoveringMapOn_eval` 📖	mathematical	—	`IsCoveringMapOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `eval` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Compl.compl` `Set` `Set.instCompl` `Set.image` `setOf` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `derivative` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing`	—	`IsClosedMap.isCoveringMapOn_of_openPartialHomeomorph` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `isClosedMap_eval` `NormMulClass.isAbsoluteValue_norm` `NormedDivisionRing.toNormMulClass` `eq_or_ne` `Set.image_congr` `eval_C` `Set.Nonempty.image_const` `derivative_C` `eval_zero` `Nontrivial.to_nonempty` `EuclideanDomain.toNontrivial` `instIsDomain` `preimage_eval_singleton` `rootSet_finite` `RingHomInvPair.ids` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `complete_of_proper` `HasStrictDerivAt.hasStrictFDerivAt_equiv` `hasStrictDerivAt` `HasStrictFDerivAt.mem_toOpenPartialHomeomorph_source`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isCoveringMapOn_npow` 📖	mathematical	—	`IsCoveringMapOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing`	—	`Polynomial.eval_pow` `Polynomial.eval_X` `IsCoveringMapOn.mono` `Polynomial.isCoveringMapOn_eval` `Set.image_congr` `Polynomial.derivative_X_pow` `map_natCast` `RingHom.instRingHomClass` `Polynomial.eval_mul` `Polynomial.eval_natCast` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `isReduced_of_noZeroDivisors` `EuclideanDomain.toNontrivial` `zero_pow` `Nat.cast_zero`
`isCoveringMapOn_zpow` 📖	mathematical	—	`IsCoveringMapOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing`	—	`zpow_eq_zero_iff` `Int.cast_zero` `IsCoveringMapOn.of_isCoveringMap_restrictPreimage` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `Set.ext` `IsClosed.isOpen_compl` `isClosed_singleton` `zpow_ne_zero` `Iff.not` `IsCoveringMap.comp_homeomorph` `isCoveringMap_zpow`
`isCoveringMap_npow` 📖	mathematical	—	`IsCoveringMap` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `pow_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedCommRing.toNormedRing` `NormedDivisionRing.toNormMulClass` `NormedField.toNormedDivisionRing`	—	`pow_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Set.ext` `Nat.cast_zero` `IsCoveringMap.comp_homeomorph` `IsCoveringMapOn.isCoveringMap_restrictPreimage` `isCoveringMapOn_npow`
`isCoveringMap_zpow` 📖	mathematical	—	`IsCoveringMap` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `instTopologicalSpaceSubtype` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `zpow_ne_zero` `DivisionSemiring.toGroupWithZero` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField`	—	`zpow_ne_zero` `pow_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `zpow_natCast` `isCoveringMap_npow` `Int.cast_natCast` `IsTopologicalDivisionRing.toContinuousInv₀` `NormedDivisionRing.to_isTopologicalDivisionRing` `zpow_neg` `inv_pow` `IsCoveringMap.comp_homeomorph` `Int.cast_neg`
`isQuotientCoveringMap_npow` 📖	mathematical	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField`	`IsQuotientCoveringMap` `Units` `Units.instTopologicalSpaceUnits` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Units.instMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.ker` `Units.instMulOneClass` `powMonoidHom` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Subgroup.toGroup` `MulAction.instMulAction` `Monoid.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`rootsOfUnity_eq_ker` `Nat.cast_zero` `IsClosedMap.isQuotientMap` `IsClosedMap.restrictPreimage` `isClosedMap_pow` `NormMulClass.isAbsoluteValue_norm` `NormedDivisionRing.toNormMulClass` `Continuous.restrictPreimage` `Continuous.pow` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `continuous_id'` `Function.Surjective.restrictPreimage` `IsTopologicalDivisionRing.toContinuousInv₀` `Set.ext` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `Equiv.left_inv` `Topology.IsQuotientMap.comp` `Homeomorph.isQuotientMap` `Topology.IsQuotientMap.isQuotientCoveringMap_of_subgroup` `Units.instIsTopologicalGroupOfContinuousMul` `Set.Finite.isDiscrete` `T2Space.t1Space` `Units.instT2Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Finite.of_fintype` `instIsDomain` `mul_pow` `inv_pow`
`isQuotientCoveringMap_zpow` 📖	mathematical	`DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NontriviallyNormedField.toNormedField`	`IsQuotientCoveringMap` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Units.instTopologicalSpaceUnits` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Units.instDivInvMonoid` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.ker` `Units.instMulOneClass` `zpowGroupHom` `CommGroup.toDivisionCommMonoid` `Units.instCommGroupUnits` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Subgroup.toGroup` `MulAction.instMulAction` `Monoid.toMulAction` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`isQuotientCoveringMap_npow` `Int.cast_natCast` `zpow_natCast` `Subgroup.ext` `zpow_neg` `IsTopologicalGroup.toContinuousInv` `Units.instIsTopologicalGroupOfContinuousMul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Units.ext` `Units.val_inv_eq_inv_val` `IsQuotientCoveringMap.homeomorph_comp` `Int.cast_neg` `inv_inv` `Function.Involutive.surjective` `inv_involutive`

---

← Back to Index