Metric

📁 Source: Mathlib/Combinatorics/SimpleGraph/Metric.lean

Statistics

Metric	Count
Definitions `dist`, `edist`	2
Theorems `diff_dist_adj`, `diff_dist_adj`, `dist_eq_zero_iff`, `dist_triangle`, `exists_path_of_dist`, `exists_walk_length_eq_dist`, `exists_walk_length_eq_edist`, `one_lt_dist_of_ne_of_not_adj`, `pos_dist_of_ne`, `coe_dist_eq_edist`, `dist_anti`, `dist_eq_zero_iff`, `dist_triangle_left`, `dist_triangle_right`, `exists_path_of_dist`, `exists_walk_length_eq_dist`, `exists_walk_length_eq_edist`, `of_dist_ne_zero`, `one_lt_dist_of_ne_of_not_adj`, `pos_dist_of_ne`, `edist_le`, `exists_adj_adj_not_adj_ne`, `isPath_of_length_eq_dist`, `dist_bot`, `dist_comm`, `dist_eq_one_iff_adj`, `dist_eq_sInf`, `dist_eq_zero_iff_eq_or_not_reachable`, `dist_eq_zero_of_not_reachable`, `dist_le`, `dist_ne_zero_iff_ne_and_reachable`, `dist_self`, `dist_top`, `dist_top_of_ne`, `edist_anti`, `edist_bot`, `edist_bot_of_ne`, `edist_comm`, `edist_eq_one_iff_adj`, `edist_eq_sInf`, `edist_eq_top_of_not_reachable`, `edist_eq_two_iff`, `edist_eq_zero_iff`, `edist_le`, `edist_le_one_iff_adj_or_eq`, `edist_ne_top_iff_reachable`, `edist_pos_of_ne`, `edist_self`, `edist_top`, `edist_top_of_ne`, `edist_triangle`, `exists_walk_of_dist_ne_zero`, `exists_walk_of_edist_eq_coe`, `exists_walk_of_edist_ne_top`, `length_eq_dist_of_subwalk`, `nonempty_of_pos_dist`, `reachable_of_edist_ne_top`, `two_lt_edist_iff`	58
Total	60

SimpleGraph

Definitions

Name	Category	Theorems
`dist` 📖	CompOp	33 math math: `length_eq_dist_of_subwalk`, `Reachable.dist_anti`, `Connected.one_lt_dist_of_ne_of_not_adj`, `Reachable.one_lt_dist_of_ne_of_not_adj`, `Connected.dist_triangle`, `Connected.exists_walk_length_eq_dist`, `dist_eq_sInf`, `dist_comm`, `dist_le_diam`, `dist_top_of_ne`, `IsTree.dist_eq_dist_add_one_of_adj`, `IsAcyclic.dist_eq_dist_add_one_of_adj_of_reachable`, `dist_self`, `dist_eq_one_iff_adj`, `Connected.exists_path_of_dist`, `dist_bot`, `dist_le`, `Connected.diff_dist_adj`, `Reachable.dist_eq_zero_iff`, `Reachable.dist_triangle_right`, `dist_eq_zero_of_not_reachable`, `Reachable.exists_walk_length_eq_dist`, `exists_dist_eq_diam`, `dist_eq_zero_iff_eq_or_not_reachable`, `Connected.dist_eq_zero_iff`, `Reachable.pos_dist_of_ne`, `Adj.diff_dist_adj`, `Reachable.dist_triangle_left`, `Reachable.coe_dist_eq_edist`, `exists_walk_of_dist_ne_zero`, `Connected.pos_dist_of_ne`, `Reachable.exists_path_of_dist`, `dist_top`
`edist` 📖	CompOp	37 math math: `ediam_le_iff`, `exists_edist_eq_ediam_of_ne_top`, `Walk.edist_le`, `ediam_eq_top`, `edist_eq_top_of_not_reachable`, `edist_self`, `edist_top`, `exists_edist_eq_radius_of_finite`, `edist_pos_of_ne`, `exists_edist_eq_eccent_of_finite`, `edist_le_eccent`, `edist_triangle`, `edist_bot`, `edist_eq_sInf`, `ediam_eq_iSup_iSup_edist`, `Connected.exists_walk_length_eq_edist`, `edist_anti`, `edist_eq_two_iff`, `diam_def`, `edist_le_ediam`, `eccent_le_iff`, `ediam_def`, `exists_walk_of_edist_ne_top`, `Reachable.coe_dist_eq_edist`, `edist_comm`, `edist_eq_zero_iff`, `edist_le`, `Reachable.exists_walk_length_eq_edist`, `two_lt_edist_iff`, `edist_top_of_ne`, `edist_boxProd`, `edist_eq_one_iff_adj`, `eccent_def`, `edist_bot_of_ne`, `exists_edist_eq_ediam_of_finite`, `edist_le_one_iff_adj_or_eq`, `radius_eq_iInf_iSup_edist`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_bot` 📖	mathematical	—	`dist` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`dist_self`
`dist_comm` 📖	mathematical	—	`dist`	—	`dist.eq_1` `edist_comm`
`dist_eq_one_iff_adj` 📖	mathematical	—	`dist` `Adj`	—	`dist.eq_1` `ENat.toNat_eq_iff` `ENat.coe_one` `edist_eq_one_iff_adj`
`dist_eq_sInf` 📖	mathematical	—	`dist` `InfSet.sInf` `Nat.instInfSet` `Set.range` `Walk` `Walk.length`	—	`ENat.iInf_toNat`
`dist_eq_zero_iff_eq_or_not_reachable` 📖	mathematical	—	`dist` `Reachable`	—	`dist_eq_sInf`
`dist_eq_zero_of_not_reachable` 📖	mathematical	`Reachable`	`dist`	—	—
`dist_le` 📖	mathematical	—	`dist` `Walk.length`	—	`Nat.sInf_le` `dist_eq_sInf`
`dist_ne_zero_iff_ne_and_reachable` 📖	mathematical	—	`Reachable`	—	—
`dist_self` 📖	mathematical	—	`dist`	—	—
`dist_top` 📖	mathematical	—	`dist` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`dist_self`
`dist_top_of_ne` 📖	mathematical	—	`dist` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	—
`edist_anti` 📖	mathematical	`SimpleGraph` `instLE`	`ENat` `instLEENat` `edist`	—	`Reachable.exists_walk_length_eq_edist` `Walk.length_map` `edist_le` `le_top` `edist_eq_top_of_not_reachable`
`edist_bot` 📖	mathematical	—	`edist` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `ENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Top.top` `instTopENat`	—	`edist_self` `edist_bot_of_ne`
`edist_bot_of_ne` 📖	mathematical	—	`edist` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Top.top` `ENat` `instTopENat`	—	`Iff.not` `edist_ne_top_iff_reachable` `reachable_bot`
`edist_comm` 📖	mathematical	—	`edist`	—	`edist_eq_sInf` `Set.image_univ` `Set.image_univ_of_surjective` `Walk.reverse_surjective` `Set.image_comp` `Walk.length_reverse`
`edist_eq_one_iff_adj` 📖	mathematical	—	`edist` `ENat` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat` `Adj`	—	`exists_walk_of_edist_ne_top` `Walk.adj_of_length_eq_one` `Nat.cast_eq_one` `le_antisymm` `edist_le` `Order.one_le_iff_pos` `NeZero.one` `edist_pos_of_ne` `Adj.ne`
`edist_eq_sInf` 📖	mathematical	—	`edist` `InfSet.sInf` `ENat` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `Set.range` `Walk` `ENat.instNatCast` `Walk.length`	—	—
`edist_eq_top_of_not_reachable` 📖	mathematical	`Reachable`	`edist` `Top.top` `ENat` `instTopENat`	—	`ENat.iInf_eq_top_of_isEmpty` `not_reachable_iff_isEmpty_walk`
`edist_eq_two_iff` 📖	mathematical	—	`edist` `ENat` `instOfNatAtLeastTwo` `ENat.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Adj` `Set.Nonempty` `commonNeighbors`	—	`Nat.instAtLeastTwoHAddOfNat` `Iff.not` `edist_eq_zero_iff` `exists_walk_of_edist_eq_coe` `mem_commonNeighbors` `Walk.adj_getVert_succ` `Nat.instNoMaxOrder` `Nat.instCanonicallyOrderedAdd` `Adj.symm` `instReflLe` `Walk.getVert_zero` `Walk.getVert_length` `le_antisymm` `Walk.edist_le` `zero_add` `ENat.le_one_iff_eq_zero_or_eq_one` `Order.le_of_lt_succ`
`edist_eq_zero_iff` 📖	mathematical	—	`edist` `ENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	—
`edist_le` 📖	mathematical	—	`ENat` `instLEENat` `edist` `ENat.instNatCast` `Walk.length`	—	`sInf_le`
`edist_le_one_iff_adj_or_eq` 📖	mathematical	—	`ENat` `instLEENat` `edist` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat` `Adj`	—	`edist_self` `edist_pos_of_ne` `LE.le.ge_iff_eq'` `Order.one_le_iff_pos` `NeZero.one` `edist_eq_one_iff_adj`
`edist_ne_top_iff_reachable` 📖	mathematical	—	`Reachable`	—	`reachable_of_edist_ne_top` `Reachable.elim`
`edist_pos_of_ne` 📖	mathematical	—	`ENat` `instLTENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `edist`	—	`pos_iff_ne_zero` `Iff.ne` `edist_eq_zero_iff`
`edist_self` 📖	mathematical	—	`edist` `ENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`edist_eq_zero_iff`
`edist_top` 📖	mathematical	—	`edist` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `ENat` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat`	—	`edist_self`
`edist_top_of_ne` 📖	mathematical	—	`edist` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `ENat` `AddMonoidWithOne.toOne` `instAddMonoidWithOneENat`	—	—
`edist_triangle` 📖	mathematical	—	`ENat` `instLEENat` `edist` `instAddENat`	—	`eq_or_ne` `top_add` `add_top` `exists_walk_of_edist_ne_top` `Nat.cast_add` `Walk.length_append` `edist_le`
`exists_walk_of_dist_ne_zero` 📖	mathematical	—	`Walk` `Walk.length` `dist`	—	`Reachable.exists_walk_length_eq_dist` `Reachable.of_dist_ne_zero`
`exists_walk_of_edist_eq_coe` 📖	mathematical	`edist` `ENat` `ENat.instNatCast`	`Walk` `Walk.length`	—	`ENat.coe_ne_top` `exists_walk_of_edist_ne_top` `Nat.cast_injective`
`exists_walk_of_edist_ne_top` 📖	mathematical	—	`Walk` `ENat` `ENat.instNatCast` `Walk.length` `edist`	—	`Reachable.exists_walk_length_eq_edist` `reachable_of_edist_ne_top`
`length_eq_dist_of_subwalk` 📖	mathematical	`Walk.length` `dist` `Walk.IsSubwalk`	`Walk.length` `dist`	—	`LE.le.eq_of_not_lt'` `dist_le` `Reachable.exists_path_of_dist` `Walk.reachable` `Walk.length_append`
`nonempty_of_pos_dist` 📖	mathematical	`dist`	`Set.Nonempty` `Walk` `Set.univ`	—	`Nat.nonempty_of_pos_sInf` `dist_eq_sInf`
`reachable_of_edist_ne_top` 📖	mathematical	—	`Reachable`	—	`Function.mt` `edist_eq_top_of_not_reachable`
`two_lt_edist_iff` 📖	mathematical	—	`ENat` `instLTENat` `instOfNatAtLeastTwo` `ENat.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `edist` `Adj` `commonNeighbors` `Set` `Set.instEmptyCollection`	—	`Nat.instAtLeastTwoHAddOfNat` `edist_self` `edist_eq_one_iff_adj` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `edist_eq_two_iff` `lt_of_le_of_ne` `one_add_one_eq_two` `Order.add_one_le_of_lt`

SimpleGraph.Adj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diff_dist_adj` 📖	mathematical	`SimpleGraph.Adj`	`SimpleGraph.dist`	—	`SimpleGraph.dist_eq_one_iff_adj` `symm` `SimpleGraph.Reachable.dist_triangle_right` `reachable` `SimpleGraph.Reachable.dist_triangle_left`

SimpleGraph.Connected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diff_dist_adj` 📖	mathematical	`SimpleGraph.Connected` `SimpleGraph.Adj`	`SimpleGraph.dist`	—	`SimpleGraph.Adj.diff_dist_adj`
`dist_eq_zero_iff` 📖	mathematical	`SimpleGraph.Connected`	`SimpleGraph.dist`	—	`preconnected`
`dist_triangle` 📖	mathematical	`SimpleGraph.Connected`	`SimpleGraph.dist`	—	`exists_walk_length_eq_dist` `SimpleGraph.Walk.length_append` `SimpleGraph.dist_le`
`exists_path_of_dist` 📖	mathematical	`SimpleGraph.Connected`	`SimpleGraph.Walk` `SimpleGraph.Walk.IsPath` `SimpleGraph.Walk.length` `SimpleGraph.dist`	—	`exists_walk_length_eq_dist` `SimpleGraph.Walk.isPath_of_length_eq_dist`
`exists_walk_length_eq_dist` 📖	mathematical	`SimpleGraph.Connected`	`SimpleGraph.Walk` `SimpleGraph.Walk.length` `SimpleGraph.dist`	—	`SimpleGraph.Reachable.exists_walk_length_eq_dist` `preconnected` `SimpleGraph.dist_eq_sInf`
`exists_walk_length_eq_edist` 📖	mathematical	`SimpleGraph.Connected`	`SimpleGraph.Walk` `ENat` `ENat.instNatCast` `SimpleGraph.Walk.length` `SimpleGraph.edist`	—	`SimpleGraph.Reachable.exists_walk_length_eq_edist` `preconnected`
`one_lt_dist_of_ne_of_not_adj` 📖	mathematical	`SimpleGraph.Connected` `SimpleGraph.Adj`	`SimpleGraph.dist`	—	`SimpleGraph.Reachable.one_lt_dist_of_ne_of_not_adj` `preconnected`
`pos_dist_of_ne` 📖	mathematical	`SimpleGraph.Connected`	`SimpleGraph.dist`	—	`dist_eq_zero_iff`

SimpleGraph.Reachable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_dist_eq_edist` 📖	mathematical	—	`ENat` `ENat.instNatCast` `SimpleGraph.dist` `SimpleGraph.edist`	—	`ENat.coe_toNat` `SimpleGraph.edist_ne_top_iff_reachable`
`dist_anti` 📖	mathematical	`SimpleGraph` `SimpleGraph.instLE`	`SimpleGraph.dist`	—	`exists_walk_length_eq_dist` `SimpleGraph.Walk.length_map` `SimpleGraph.dist_le`
`dist_eq_zero_iff` 📖	mathematical	—	`SimpleGraph.dist`	—	—
`dist_triangle_left` 📖	mathematical	—	`SimpleGraph.dist`	—	`ENat.coe_le_coe` `ENat.coe_add`
`dist_triangle_right` 📖	mathematical	—	`SimpleGraph.dist`	—	`ENat.coe_le_coe` `ENat.coe_add`
`exists_path_of_dist` 📖	mathematical	—	`SimpleGraph.Walk` `SimpleGraph.Walk.IsPath` `SimpleGraph.Walk.length` `SimpleGraph.dist`	—	`exists_walk_length_eq_dist` `SimpleGraph.Walk.isPath_of_length_eq_dist`
`exists_walk_length_eq_dist` 📖	mathematical	—	`SimpleGraph.Walk` `SimpleGraph.Walk.length` `SimpleGraph.dist`	—	`Nat.sInf_mem` `Set.range_nonempty_iff_nonempty` `SimpleGraph.dist_eq_sInf`
`exists_walk_length_eq_edist` 📖	mathematical	—	`SimpleGraph.Walk` `ENat` `ENat.instNatCast` `SimpleGraph.Walk.length` `SimpleGraph.edist`	—	`csInf_mem` `Set.range_nonempty_iff_nonempty`
`of_dist_ne_zero` 📖	mathematical	—	`SimpleGraph.Reachable`	—	`SimpleGraph.dist_ne_zero_iff_ne_and_reachable`
`one_lt_dist_of_ne_of_not_adj` 📖	mathematical	`SimpleGraph.Adj`	`SimpleGraph.dist`	—	`pos_dist_of_ne` `exists_walk_length_eq_dist` `SimpleGraph.Walk.exists_length_eq_one_iff`
`pos_dist_of_ne` 📖	mathematical	—	`SimpleGraph.dist`	—	—

SimpleGraph.Walk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`edist_le` 📖	mathematical	—	`ENat` `instLEENat` `SimpleGraph.edist` `ENat.instNatCast` `length`	—	`SimpleGraph.edist_le`
`exists_adj_adj_not_adj_ne` 📖	mathematical	`length` `SimpleGraph.dist`	`SimpleGraph.Adj`	—	`length_tail_add_one` `getVert_tail` `SimpleGraph.dist_le` `adj_snd` `adj_getVert_succ`
`isPath_of_length_eq_dist` 📖	mathematical	`length` `SimpleGraph.dist`	`IsPath`	—	`bypass_eq_self_of_length_le` `SimpleGraph.dist_le` `bypass_isPath`

---

← Back to Index