Documentation Verification Report

Gluing

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

Statistics

Metric	Count
Definitions `GlueSpace`, `InductiveLimit`, `dist`, `instDist`, `metricSpace`, `dist`, `glueDist`, `glueMetricApprox`, `gluePremetric`, `inductiveLimitDist`, `inductivePremetric`, `inhabitedLeft`, `inhabitedRight`, `instInhabitedInductiveLimitOfOfNatNat`, `instMetricSpaceGlueSpace`, `instMetricSpaceInductiveLimit`, `metricSpaceSum`, `toGlueL`, `toGlueR`, `toInductiveLimit`	20
Theorems `completeSpace`, `dist_ne`, `dist_same`, `dist_triangle`, `fst_eq_of_dist_lt_one`, `isOpen_iff`, `isometry_mk`, `one_le_dist_of_ne`, `dist_eq`, `dist_eq_glueDist`, `mem_uniformity_iff_glueDist`, `one_le_dist_inl_inr`, `one_le_dist_inr_inl`, `dense_iUnion_range_toInductiveLimit`, `glueDist_glued_points`, `glueDist_swap`, `inductiveLimitDist_eq_dist`, `isometry_inl`, `isometry_inr`, `le_glueDist_inl_inr`, `le_glueDist_inr_inl`, `separableSpaceInductiveLimit_of_separableSpace`, `toGlueL_isometry`, `toGlueR_isometry`, `toGlue_commute`, `toInductiveLimit_commute`, `toInductiveLimit_isometry`	27
Total	47

Metric

Definitions

Name	Category	Theorems
`GlueSpace` 📖	CompOp	3 math math: `toGlueL_isometry`, `toGlue_commute`, `toGlueR_isometry`
`InductiveLimit` 📖	CompOp	4 math math: `separableSpaceInductiveLimit_of_separableSpace`, `toInductiveLimit_commute`, `dense_iUnion_range_toInductiveLimit`, `toInductiveLimit_isometry`
`glueDist` 📖	CompOp	5 math math: `glueDist_glued_points`, `le_glueDist_inr_inl`, `glueDist_swap`, `le_glueDist_inl_inr`, `Sum.dist_eq_glueDist`
`glueMetricApprox` 📖	CompOp	—
`gluePremetric` 📖	CompOp	—
`inductiveLimitDist` 📖	CompOp	1 math math: `inductiveLimitDist_eq_dist`
`inductivePremetric` 📖	CompOp	—
`inhabitedLeft` 📖	CompOp	—
`inhabitedRight` 📖	CompOp	—
`instInhabitedInductiveLimitOfOfNatNat` 📖	CompOp	—
`instMetricSpaceGlueSpace` 📖	CompOp	2 math math: `toGlueL_isometry`, `toGlueR_isometry`
`instMetricSpaceInductiveLimit` 📖	CompOp	3 math math: `separableSpaceInductiveLimit_of_separableSpace`, `dense_iUnion_range_toInductiveLimit`, `toInductiveLimit_isometry`
`metricSpaceSum` 📖	CompOp	3 math math: `isometry_inl`, `Sum.dist_eq`, `isometry_inr`
`toGlueL` 📖	CompOp	2 math math: `toGlueL_isometry`, `toGlue_commute`
`toGlueR` 📖	CompOp	2 math math: `toGlue_commute`, `toGlueR_isometry`
`toInductiveLimit` 📖	CompOp	3 math math: `toInductiveLimit_commute`, `dense_iUnion_range_toInductiveLimit`, `toInductiveLimit_isometry`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dense_iUnion_range_toInductiveLimit` 📖	mathematical	`Isometry` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	`Dense` `InductiveLimit` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `instMetricSpaceInductiveLimit` `Set.iUnion` `Set.range` `toInductiveLimit`	—	`Dense.mono` `Set.mem_iUnion` `Set.mem_range` `dense_univ`
`glueDist_glued_points` 📖	mathematical	—	`glueDist`	—	`add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `dist_nonneg` `le_antisymm` `dist_self` `add_zero` `ciInf_le` `Set.forall_mem_range` `le_ciInf` `zero_add`
`glueDist_swap` 📖	mathematical	—	`glueDist`	—	`add_comm`
`inductiveLimitDist_eq_dist` 📖	mathematical	`Isometry` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	`inductiveLimitDist` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Nat.leRecOn`	—	`nonpos_iff_eq_zero` `Nat.instCanonicallyOrderedAdd` `Nat.of_le_succ` `le_trans` `le_max_left` `le_max_right` `Nat.leRecOn_succ` `Isometry.dist_eq`
`isometry_inl` 📖	mathematical	—	`Isometry` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `metricSpaceSum`	—	`Isometry.of_dist_eq`
`isometry_inr` 📖	mathematical	—	`Isometry` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `metricSpaceSum`	—	`Isometry.of_dist_eq`
`le_glueDist_inl_inr` 📖	mathematical	—	`Real` `Real.instLE` `glueDist`	—	`le_add_of_nonneg_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.iInf_nonneg` `add_nonneg` `dist_nonneg`
`le_glueDist_inr_inl` 📖	mathematical	—	`Real` `Real.instLE` `glueDist`	—	`le_glueDist_inl_inr`
`separableSpaceInductiveLimit_of_separableSpace` 📖	mathematical	`TopologicalSpace.SeparableSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `Isometry` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	`InductiveLimit` `instMetricSpaceInductiveLimit`	—	`Set.countable_iUnion` `instCountableNat` `Set.Countable.image` `Dense.of_closure` `Dense.mono` `Set.iUnion_subset` `Continuous.range_subset_closure_image_dense` `Isometry.continuous` `toInductiveLimit_isometry` `closure_mono` `Set.subset_iUnion` `dense_iUnion_range_toInductiveLimit` `TopologicalSpace.exists_countable_dense`
`toGlueL_isometry` 📖	mathematical	`Isometry` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	`GlueSpace` `instMetricSpaceGlueSpace` `toGlueL`	—	`Isometry.of_dist_eq`
`toGlueR_isometry` 📖	mathematical	`Isometry` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	`GlueSpace` `instMetricSpaceGlueSpace` `toGlueR`	—	`Isometry.of_dist_eq`
`toGlue_commute` 📖	mathematical	`Isometry` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	`GlueSpace` `toGlueL` `toGlueR`	—	`inseparable_iff` `glueDist_glued_points`
`toInductiveLimit_commute` 📖	mathematical	`Isometry` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	`InductiveLimit` `toInductiveLimit`	—	`inseparable_iff` `le_refl` `inductiveLimitDist_eq_dist` `Nat.leRecOn_self` `Nat.leRecOn_succ` `dist_self`
`toInductiveLimit_isometry` 📖	mathematical	`Isometry` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace`	`InductiveLimit` `instMetricSpaceInductiveLimit` `toInductiveLimit`	—	`Isometry.of_dist_eq` `le_refl` `inductiveLimitDist_eq_dist` `Nat.leRecOn_self`

Metric.Sigma

Definitions

Name	Category	Theorems
`dist` 📖	CompOp	—
`instDist` 📖	CompOp	4 math math: `one_le_dist_of_ne`, `dist_triangle`, `dist_ne`, `dist_same`
`metricSpace` 📖	CompOp	2 math math: `completeSpace`, `isometry_mk`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeSpace` 📖	mathematical	`CompleteSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace`	`metricSpace`	—	`IsUniformInducing.isComplete_range` `Isometry.isUniformInducing` `fst_eq_of_dist_lt_one` `completeSpace_of_isComplete_univ` `Set.iUnion_of_singleton` `isComplete_iUnion_separated` `Metric.dist_mem_uniformity` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing`
`dist_ne` 📖	mathematical	—	`Dist.dist` `instDist` `Real` `Real.instAdd` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Nonempty.some` `Real.instOne`	—	—
`dist_same` 📖	mathematical	—	`Dist.dist` `instDist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace`	—	—
`dist_triangle` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `instDist` `Real.instAdd`	—	`eq_or_ne` `dist_same` `dist_triangle` `dist_ne` `add_zero` `zero_add` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `le_rfl` `zero_le_one` `Real.instZeroLEOneClass` `dist_nonneg` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.term_add_constg`
`fst_eq_of_dist_lt_one` 📖	—	`Real` `Real.instLT` `Dist.dist` `instDist` `Real.instOne`	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `one_le_dist_of_ne`
`isOpen_iff` 📖	mathematical	—	`IsOpen` `instTopologicalSpaceSigma` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `Real` `Real.instLT` `Real.instZero` `Set` `Set.instMembership`	—	`Metric.isOpen_iff` `isOpen_sigma_iff` `lt_min` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `eq_or_ne` `Metric.mem_ball'` `dist_same` `lt_irrefl` `one_le_dist_of_ne` `LT.lt.trans_le` `min_le_right`
`isometry_mk` 📖	mathematical	—	`Isometry` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `metricSpace`	—	`Isometry.of_dist_eq` `dist_same`
`one_le_dist_of_ne` 📖	mathematical	—	`Real` `Real.instLE` `Real.instOne` `Dist.dist` `instDist`	—	`dist_ne` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `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_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `dist_nonneg`

Metric.Sum

Definitions

Name	Category	Theorems
`dist` 📖	CompOp	4 math math: `one_le_dist_inr_inl`, `one_le_dist_inl_inr`, `dist_eq_glueDist`, `dist_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_eq` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `Metric.metricSpaceSum` `dist`	—	—
`dist_eq_glueDist` 📖	mathematical	—	`dist` `Metric.glueDist` `Nonempty.some` `Real` `Real.instOne`	—	`dist_comm` `add_comm` `add_left_comm` `ciInf_unique` `add_assoc`
`mem_uniformity_iff_glueDist` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Set` `Filter` `Filter.instMembership` `uniformity` `Sum.instUniformSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `Set.instMembership`	—	`lt_min` `LE.le.not_gt` `Metric.le_glueDist_inl_inr` `Metric.le_glueDist_inr_inl`
`one_le_dist_inl_inr` 📖	mathematical	—	`Real` `Real.instLE` `Real.instOne` `dist`	—	`dist.eq_3` `le_imp_le_of_le_of_le` `le_refl` `le_add_of_nonneg_right` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `dist_nonneg` `le_add_of_nonneg_left` `covariant_swap_add_of_covariant_add`
`one_le_dist_inr_inl` 📖	mathematical	—	`Real` `Real.instLE` `Real.instOne` `dist`	—	`one_le_dist_inl_inr`

---

← Back to Index