Documentation Verification Report

MazurUlam

📁 Source: Mathlib/Analysis/Normed/Affine/MazurUlam.lean

Statistics

Metric	Count
Definitions `toRealAffineIsometryEquiv`, `toRealLinearIsometryEquiv`, `toRealLinearIsometryEquivOfMapZero`	3
Theorems `coeFn_toRealAffineIsometryEquiv`, `coe_toRealAffineIsometryEquiv`, `coe_toRealLinearIsometryEquivOfMapZero`, `coe_toRealLinearIsometryEquivOfMapZero_symm`, `map_midpoint`, `midpoint_fixed`, `toRealLinearIsometryEquiv_apply`, `toRealLinearIsometryEquiv_symm_apply`	8
Total	11

IsometryEquiv

Definitions

Name	Category	Theorems
`toRealAffineIsometryEquiv` 📖	CompOp	2 math math: `coe_toRealAffineIsometryEquiv`, `coeFn_toRealAffineIsometryEquiv`
`toRealLinearIsometryEquiv` 📖	CompOp	2 math math: `toRealLinearIsometryEquiv_symm_apply`, `toRealLinearIsometryEquiv_apply`
`toRealLinearIsometryEquivOfMapZero` 📖	CompOp	2 math math: `coe_toRealLinearIsometryEquivOfMapZero`, `coe_toRealLinearIsometryEquivOfMapZero_symm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeFn_toRealAffineIsometryEquiv` 📖	mathematical	—	`DFunLike.coe` `AffineIsometryEquiv` `Real` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `MetricSpace.toPseudoMetricSpace` `EquivLike.toFunLike` `AffineIsometryEquiv.instEquivLike` `toRealAffineIsometryEquiv` `IsometryEquiv` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `instEquivLike`	—	—
`coe_toRealAffineIsometryEquiv` 📖	mathematical	—	`AffineIsometryEquiv.toIsometryEquiv` `Real` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `MetricSpace.toPseudoMetricSpace` `toRealAffineIsometryEquiv`	—	`ext`
`coe_toRealLinearIsometryEquivOfMapZero` 📖	mathematical	`DFunLike.coe` `IsometryEquiv` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `EquivLike.toFunLike` `instEquivLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`LinearIsometryEquiv` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `LinearIsometryEquiv.instEquivLike` `toRealLinearIsometryEquivOfMapZero`	—	`RingHomInvPair.ids`
`coe_toRealLinearIsometryEquivOfMapZero_symm` 📖	mathematical	`DFunLike.coe` `IsometryEquiv` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `EquivLike.toFunLike` `instEquivLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`LinearIsometryEquiv` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `toRealLinearIsometryEquivOfMapZero` `symm`	—	`RingHomInvPair.ids`
`map_midpoint` 📖	mathematical	—	`DFunLike.coe` `IsometryEquiv` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `EquivLike.toFunLike` `instEquivLike` `midpoint` `Real` `Real.instRing` `invertibleTwo` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.instField` `IsStrictOrderedRing.toCharZero` `DivisionSemiring.toSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace`	—	`IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `AffineIsometryEquiv.pointReflection_midpoint_left` `symm_apply_apply` `AffineIsometryEquiv.pointReflection_midpoint_right` `midpoint_fixed` `AffineIsometryEquiv.pointReflection_fixed_iff` `symm_apply_eq` `AffineIsometryEquiv.pointReflection_self` `AffineIsometryEquiv.coe_toIsometryEquiv` `AffineIsometryEquiv.pointReflection_symm` `AffineIsometryEquiv.toIsometryEquiv_symm` `eq_symm_apply`
`midpoint_fixed` 📖	mathematical	`DFunLike.coe` `IsometryEquiv` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `EquivLike.toFunLike` `instEquivLike`	`midpoint` `Real` `Real.instRing` `invertibleTwo` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.instField` `IsStrictOrderedRing.toCharZero` `DivisionSemiring.toSemiring` `Real.partialOrder` `Real.instIsStrictOrderedRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace`	—	`IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Set.forall_mem_range` `dist_triangle` `dist_comm` `dist_eq` `Nat.instAtLeastTwoHAddOfNat` `AffineIsometryEquiv.dist_pointReflection_fixed` `apply_symm_apply` `AffineIsometryEquiv.dist_pointReflection_self_real` `AffineIsometryEquiv.pointReflection_midpoint_left` `symm_apply_eq` `AffineIsometryEquiv.pointReflection_midpoint_right` `ciSup_le` `le_div_iff₀'` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `zero_lt_two'` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `le_ciSup` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `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.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.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `CancelDenoms.sub_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_nonpos` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Meta.NormNum.isNat_lt_true` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `dist_le_zero` `le_trans`
`toRealLinearIsometryEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `toRealLinearIsometryEquiv` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `IsometryEquiv` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `instEquivLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`sub_eq_add_neg`
`toRealLinearIsometryEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `LinearIsometryEquiv` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `LinearIsometryEquiv.symm` `toRealLinearIsometryEquiv` `IsometryEquiv` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `instEquivLike` `symm` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`RingHomInvPair.ids`

---

← Back to Index