Documentation Verification Report

Basic

📁 Source: Mathlib/Topology/MetricSpace/Ultra/Basic.lean

Statistics

Metric	Count
Definitions `IsUltrametricDist`	1
Theorems `ball_eq_of_mem`, `ball_eq_or_disjoint`, `ball_subset_trichotomy`, `closedBall_eq_of_mem`, `closedBall_eq_or_disjoint`, `closedBall_subset_trichotomy`, `dist_eq_max_of_dist_ne_dist`, `dist_triangle_max`, `frontier_ball_eq_empty`, `frontier_closedBall_eq_empty`, `isClopen_ball`, `isClopen_closedBall`, `isClopen_sphere`, `isClosed_ball`, `isOpen_closedBall`, `isOpen_sphere`, `mem_ball_iff`, `mem_closedBall_iff`, `subtype`, `dist_triangle_max`	20
Total	21

IsUltrametricDist

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ball_eq_of_mem` 📖	—	`Set` `Set.instMembership` `Metric.ball`	—	—	`Set.ext` `LE.le.trans_lt` `dist_triangle_max` `max_lt` `dist_comm`
`ball_eq_or_disjoint` 📖	mathematical	—	`Metric.ball` `Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`ball_eq_of_mem` `Set.inter_subset_left` `Set.Nonempty.some_mem` `Set.inter_subset_right` `Set.disjoint_or_nonempty_inter`
`ball_subset_trichotomy` 📖	mathematical	—	`Set` `Set.instHasSubset` `Metric.ball` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`Set.mem_inter_iff` `Set.Nonempty.some_mem` `Metric.ball_subset_ball` `ball_eq_of_mem` `Set.disjoint_or_nonempty_inter` `disjoint_comm` `LT.lt.le`
`closedBall_eq_of_mem` 📖	—	`Set` `Set.instMembership` `Metric.closedBall`	—	—	`Set.ext` `LE.le.trans` `dist_triangle_max` `max_le` `dist_comm`
`closedBall_eq_or_disjoint` 📖	mathematical	—	`Metric.closedBall` `Disjoint` `Set` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`closedBall_eq_of_mem` `Set.inter_subset_left` `Set.Nonempty.some_mem` `Set.inter_subset_right` `Set.disjoint_or_nonempty_inter`
`closedBall_subset_trichotomy` 📖	mathematical	—	`Set` `Set.instHasSubset` `Metric.closedBall` `Disjoint` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice`	—	`Set.mem_inter_iff` `Set.Nonempty.some_mem` `Metric.closedBall_subset_closedBall` `closedBall_eq_of_mem` `Set.disjoint_or_nonempty_inter` `disjoint_comm` `LT.lt.le`
`dist_eq_max_of_dist_ne_dist` 📖	mathematical	—	`Dist.dist` `PseudoMetricSpace.toDist` `Real` `Real.instMax`	—	`le_antisymm` `dist_triangle_max` `Ne.lt_or_gt` `max_eq_right` `LT.lt.le` `le_max_iff` `dist_comm` `max_eq_left`
`dist_triangle_max` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `Real.instMax`	—	—
`frontier_ball_eq_empty` 📖	mathematical	—	`frontier` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Metric.ball` `Set` `Set.instEmptyCollection`	—	`isClopen_iff_frontier_eq_empty` `isClopen_ball`
`frontier_closedBall_eq_empty` 📖	mathematical	—	`frontier` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Metric.closedBall` `Set` `Set.instEmptyCollection`	—	`isClopen_iff_frontier_eq_empty` `isClopen_closedBall`
`isClopen_ball` 📖	mathematical	—	`IsClopen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Metric.ball`	—	`isClosed_ball` `Metric.isOpen_ball`
`isClopen_closedBall` 📖	mathematical	—	`IsClopen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Metric.closedBall`	—	`Metric.isClosed_closedBall` `isOpen_closedBall`
`isClopen_sphere` 📖	mathematical	—	`IsClopen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Metric.sphere`	—	`Metric.isClosed_sphere` `isOpen_sphere`
`isClosed_ball` 📖	mathematical	—	`IsClosed` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Metric.ball`	—	`le_or_gt` `Metric.ball_eq_empty` `isOpen_compl_iff` `Metric.isOpen_iff` `ball_eq_or_disjoint` `dist_self` `LT.lt.not_ge`
`isOpen_closedBall` 📖	mathematical	—	`IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Metric.closedBall`	—	`lt_or_gt_of_ne` `Metric.closedBall_eq_empty` `Metric.isOpen_iff` `closedBall_eq_or_disjoint` `closedBall_eq_of_mem` `LT.lt.not_gt`
`isOpen_sphere` 📖	mathematical	—	`IsOpen` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Metric.sphere`	—	`Metric.closedBall_diff_ball` `sdiff_eq` `IsOpen.inter` `isOpen_closedBall` `IsClosed.isOpen_compl` `isClosed_ball`
`mem_ball_iff` 📖	mathematical	—	`Set` `Set.instMembership` `Metric.ball`	—	`Metric.mem_ball_comm`
`mem_closedBall_iff` 📖	mathematical	—	`Set` `Set.instMembership` `Metric.closedBall`	—	`Metric.mem_closedBall_comm`
`subtype` 📖	mathematical	—	`IsUltrametricDist` `PseudoMetricSpace.toDist` `Subtype.pseudoMetricSpace`	—	`dist_triangle_max`

(root)

Definitions

Name	Category	Theorems
`IsUltrametricDist` 📖	CompData	24 math math: `Valued.instIsUltrametricDist`, `IsUltrametricDist.isUltrametricDist_of_forall_norm_add_le_max_norm`, `ContinuousMap.isUltrametricDist`, `isUltrametricDist_iff_forall_norm_natCast_le_one`, `IsUltrametricDist.of_normedAlgebra'`, `IsUltrametricDist.isUltrametricDist_iff_isNonarchimedean_norm`, `IsUltrametricDist.isUltrametricDist_of_forall_norm_sub_one_of_norm_le_one`, `IsUltrametricDist.isUltrametricDist_of_forall_pow_norm_le_nsmul_pow_max_one_norm`, `IsUltrametricDist.isUltrametricDist_of_forall_norm_add_one_le_max_norm_one`, `Padic.instIsUltrametricDist`, `IsUltrametricDist.isUltrametricDist_of_forall_nnnorm_add_le_max_nnnorm`, `IsUltrametricDist.subtype`, `IsUltrametricDist.of_normedAlgebra`, `PadicInt.instIsUltrametricDist`, `IsUltrametricDist.isUltrametricDist_of_forall_norm_add_one_of_norm_le_one`, `IsUltrametricDist.isUltrametricDist_of_forall_norm_natCast_le_one`, `IsUltrametricDist.isUltrametricDist_iff_isNonarchimedean_nnnorm`, `IsUltrametricDist.normedAlgebra_iff`, `AddGroupSeminormClass.isUltrametricDist`, `PadicAlgCl.instIsUltrametricDist`, `IsUltrametricDist.isUltrametricDist_of_forall_norm_mul_le_max_norm`, `IsUltrametricDist.isUltrametricDist_of_forall_nnnorm_mul_le_max_nnnorm`, `IsUltrametricDist.isUltrametricDist_of_isNonarchimedean_nnnorm`, `IsUltrametricDist.isUltrametricDist_of_isNonarchimedean_norm`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_triangle_max` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `Real.instMax`	—	`IsUltrametricDist.dist_triangle_max`

---

← Back to Index