Dist

📁 Source: Mathlib/Data/Nat/Dist.lean

Statistics

Metric	Count
Definitions `Dist`, `dist`	2
Theorems `triangle_inequality`, `dist_add_add_left`, `dist_add_add_right`, `dist_comm`, `dist_eq_intro`, `dist_eq_max_sub_min`, `dist_eq_sub_of_le`, `dist_eq_sub_of_le_right`, `dist_eq_zero`, `dist_mul_left`, `dist_mul_right`, `dist_pos_of_ne`, `dist_self`, `dist_succ_succ`, `dist_tri_left`, `dist_tri_left'`, `dist_tri_right`, `dist_tri_right'`, `dist_zero_left`, `dist_zero_right`, `eq_of_dist_eq_zero`	21
Total	23

Nat

Definitions

Name	Category	Theorems
`dist` 📖	CompOp	22 math math: `dist_eq_zero`, `dist.triangle_inequality`, `dist_tri_left'`, `Ordnode.Raised.dist_le`, `dist_add_add_right`, `Ordnode.Raised.dist_le'`, `dist_eq_sub_of_le_right`, `dist_add_add_left`, `dist_pos_of_ne`, `dist_eq_sub_of_le`, `dist_comm`, `dist_zero_right`, `dist_tri_right`, `dist_mul_left`, `dist_tri_left`, `dist_eq_max_sub_min`, `dist_zero_left`, `dist_self`, `dist_mul_right`, `dist_tri_right'`, `dist_eq_intro`, `dist_succ_succ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_add_add_left` 📖	mathematical	—	`dist`	—	—
`dist_add_add_right` 📖	mathematical	—	`dist`	—	—
`dist_comm` 📖	mathematical	—	`dist`	—	`add_comm`
`dist_eq_intro` 📖	mathematical	—	`dist`	—	—
`dist_eq_max_sub_min` 📖	mathematical	—	`dist`	—	`le_total` `zero_add` `sup_of_le_right` `inf_of_le_left` `add_zero` `sup_of_le_left` `inf_of_le_right`
`dist_eq_sub_of_le` 📖	mathematical	—	`dist`	—	—
`dist_eq_sub_of_le_right` 📖	mathematical	—	`dist`	—	—
`dist_eq_zero` 📖	mathematical	—	`dist`	—	—
`dist_mul_left` 📖	mathematical	—	`dist`	—	`mul_comm` `dist_mul_right`
`dist_mul_right` 📖	mathematical	—	`dist`	—	`dist.eq_1` `right_distrib` `Distrib.rightDistribClass` `tsub_mul` `instCanonicallyOrderedAdd` `instOrderedSub` `LE.total` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `covariant_swap_mul_of_covariant_mul` `instMulLeftMono`
`dist_pos_of_ne` 📖	mathematical	—	`dist`	—	—
`dist_self` 📖	mathematical	—	`dist`	—	`tsub_self` `instCanonicallyOrderedAdd` `instOrderedSub` `add_zero`
`dist_succ_succ` 📖	mathematical	—	`dist`	—	—
`dist_tri_left` 📖	mathematical	—	`dist`	—	—
`dist_tri_left'` 📖	mathematical	—	`dist`	—	—
`dist_tri_right` 📖	mathematical	—	`dist`	—	—
`dist_tri_right'` 📖	mathematical	—	`dist`	—	—
`dist_zero_left` 📖	mathematical	—	`dist`	—	—
`dist_zero_right` 📖	mathematical	—	`dist`	—	—
`eq_of_dist_eq_zero` 📖	—	`dist`	—	—	—

Nat.dist

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`triangle_inequality` 📖	mathematical	—	`Nat.dist`	—	—

(root)

Definitions

Name	Category	Theorems
`Dist` 📖	CompData	—

---

← Back to Index