Diam

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

Statistics

Metric	Count
Definitions `center`, `diam`, `eccent`, `ediam`, `radius`	5
Theorems `center_bot`, `center_eq_univ_iff_radius_eq_ediam`, `center_eq_univ_of_subsingleton`, `center_nonempty`, `center_top`, `connected_iff_diam_ne_zero`, `connected_iff_ediam_ne_top`, `connected_of_ediam_ne_top`, `diam_anti_of_ediam_ne_top`, `diam_bot`, `diam_def`, `diam_eq_one`, `diam_eq_zero`, `diam_eq_zero_iff_ediam_eq_top`, `diam_eq_zero_of_ediam_eq_top`, `diam_eq_zero_of_not_connected`, `diam_ne_zero_of_ediam_ne_top`, `diam_top`, `dist_le_diam`, `eccent_bot`, `eccent_def`, `eccent_eq_one_iff`, `eccent_eq_top_of_not_connected`, `eccent_eq_zero_iff`, `eccent_eq_zero_of_subsingleton`, `eccent_le_ediam`, `eccent_le_iff`, `eccent_le_one_iff`, `eccent_ne_zero`, `eccent_pos_iff`, `eccent_top`, `ediam_anti`, `ediam_bot`, `ediam_def`, `ediam_eq_iSup_iSup_edist`, `ediam_eq_one`, `ediam_eq_top`, `ediam_eq_top_of_not_connected`, `ediam_eq_top_of_not_preconnected`, `ediam_eq_zero_iff_subsingleton`, `ediam_eq_zero_of_subsingleton`, `ediam_le_iff`, `ediam_le_of_edist_le`, `ediam_le_two_mul_radius`, `ediam_ne_top_of_diam_ne_zero`, `ediam_ne_zero`, `ediam_ne_zero_iff_nontrivial`, `ediam_top`, `edist_le_eccent`, `edist_le_ediam`, `eq_top_iff_forall_eccent_eq_one`, `exists_dist_eq_diam`, `exists_eccent_eq_ediam_of_finite`, `exists_eccent_eq_ediam_of_ne_top`, `exists_eccent_eq_radius`, `exists_edist_eq_eccent_of_finite`, `exists_edist_eq_ediam_of_finite`, `exists_edist_eq_ediam_of_ne_top`, `exists_edist_eq_radius_of_finite`, `mem_center_iff`, `nontrivial_of_diam_ne_zero`, `nontrivial_of_ediam_ne_zero`, `preconnected_of_ediam_ne_top`, `radius_bot`, `radius_eq_ediam_iff`, `radius_eq_iInf_iSup_edist`, `radius_eq_top_of_isEmpty`, `radius_eq_top_of_not_connected`, `radius_eq_zero_iff`, `radius_le_eccent`, `radius_le_ediam`, `radius_ne_top_iff`, `radius_ne_zero_of_nontrivial`, `radius_top`, `subsingleton_of_ediam_eq_zero`	75
Total	80

SimpleGraph

Definitions

Name	Category	Theorems
`center` 📖	CompOp	6 math math: `center_bot`, `center_eq_univ_of_subsingleton`, `center_nonempty`, `mem_center_iff`, `center_eq_univ_iff_radius_eq_ediam`, `center_top`
`diam` 📖	CompOp	11 math math: `diam_eq_zero_iff_ediam_eq_top`, `diam_eq_zero_of_ediam_eq_top`, `dist_le_diam`, `diam_eq_one`, `diam_bot`, `diam_def`, `diam_top`, `diam_anti_of_ediam_ne_top`, `exists_dist_eq_diam`, `diam_eq_zero_of_not_connected`, `diam_eq_zero`
`eccent` 📖	CompOp	20 math math: `eccent_bot`, `exists_eccent_eq_ediam_of_finite`, `eccent_eq_top_of_not_connected`, `eccent_le_one_iff`, `eccent_eq_zero_iff`, `exists_edist_eq_eccent_of_finite`, `eccent_eq_one_iff`, `mem_center_iff`, `edist_le_eccent`, `eccent_le_ediam`, `eccent_pos_iff`, `radius_eq_ediam_iff`, `eq_top_iff_forall_eccent_eq_one`, `eccent_le_iff`, `exists_eccent_eq_ediam_of_ne_top`, `radius_le_eccent`, `exists_eccent_eq_radius`, `eccent_def`, `eccent_eq_zero_of_subsingleton`, `eccent_top`
`ediam` 📖	CompOp	25 math math: `ediam_le_iff`, `ediam_anti`, `exists_edist_eq_ediam_of_ne_top`, `diam_eq_zero_iff_ediam_eq_top`, `exists_eccent_eq_ediam_of_finite`, `ediam_eq_top`, `ediam_top`, `ediam_eq_one`, `ediam_eq_zero_of_subsingleton`, `center_eq_univ_iff_radius_eq_ediam`, `ediam_le_two_mul_radius`, `eccent_le_ediam`, `ediam_eq_iSup_iSup_edist`, `radius_eq_ediam_iff`, `ediam_eq_zero_iff_subsingleton`, `ediam_eq_top_of_not_connected`, `edist_le_ediam`, `ediam_le_of_edist_le`, `radius_le_ediam`, `ediam_eq_top_of_not_preconnected`, `ediam_def`, `exists_eccent_eq_ediam_of_ne_top`, `diam_eq_zero`, `ediam_bot`, `exists_edist_eq_ediam_of_finite`
`radius` 📖	CompOp	14 math math: `radius_eq_zero_iff`, `exists_edist_eq_radius_of_finite`, `mem_center_iff`, `center_eq_univ_iff_radius_eq_ediam`, `ediam_le_two_mul_radius`, `radius_eq_ediam_iff`, `radius_le_ediam`, `radius_le_eccent`, `radius_eq_top_of_not_connected`, `radius_top`, `radius_bot`, `radius_eq_top_of_isEmpty`, `exists_eccent_eq_radius`, `radius_eq_iInf_iSup_edist`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`center_bot` 📖	mathematical	—	`center` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Set.univ`	—	`subsingleton_or_nontrivial` `center_eq_univ_of_subsingleton` `Set.eq_univ_iff_forall` `mem_center_iff` `eccent_bot` `radius_bot`
`center_eq_univ_iff_radius_eq_ediam` 📖	mathematical	—	`center` `Set.univ` `radius` `ediam`	—	`radius_eq_ediam_iff` `Set.univ_subset_iff` `mem_center_iff` `le_antisymm` `le_iInf` `Eq.ge` `radius_le_eccent`
`center_eq_univ_of_subsingleton` 📖	mathematical	—	`center` `Set.univ`	—	`Set.eq_univ_iff_forall` `mem_center_iff` `eccent_eq_zero_of_subsingleton` `radius_eq_zero_iff`
`center_nonempty` 📖	mathematical	—	`Set.Nonempty` `center`	—	`exists_eccent_eq_radius`
`center_top` 📖	mathematical	—	`center` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Set.univ`	—	`subsingleton_or_nontrivial` `center_eq_univ_of_subsingleton` `Set.eq_univ_iff_forall` `mem_center_iff` `eccent_top` `radius_top`
`connected_iff_diam_ne_zero` 📖	mathematical	—	`Connected`	—	`connected_iff_ediam_ne_top` `Nontrivial.to_nonempty` `not_iff_not` `diam_eq_zero_iff_ediam_eq_top`
`connected_iff_ediam_ne_top` 📖	mathematical	—	`Connected`	—	`exists_edist_eq_ediam_of_finite` `edist_ne_top_iff_reachable` `Connected.preconnected` `connected_of_ediam_ne_top`
`connected_of_ediam_ne_top` 📖	mathematical	—	`Connected`	—	`connected_iff` `preconnected_of_ediam_ne_top`
`diam_anti_of_ediam_ne_top` 📖	mathematical	`SimpleGraph` `instLE`	`diam`	—	`ENat.toNat_le_toNat` `ediam_anti`
`diam_bot` 📖	mathematical	—	`diam` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`diam.eq_1` `ENat.toNat_eq_zero` `subsingleton_or_nontrivial` `ediam_eq_zero_of_subsingleton` `ediam_bot`
`diam_def` 📖	mathematical	—	`diam` `ENat.toNat` `iSup` `ENat` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `edist`	—	`diam.eq_1` `ediam_def`
`diam_eq_one` 📖	mathematical	—	`diam` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`diam.eq_1` `ENat.toNat_eq_iff` `one_ne_zero` `Nat.cast_one` `ediam_eq_one`
`diam_eq_zero` 📖	mathematical	—	`diam` `ediam` `Top.top` `ENat` `instTopENat`	—	`diam.eq_1` `ENat.toNat_eq_zero` `ediam_eq_zero_iff_subsingleton`
`diam_eq_zero_iff_ediam_eq_top` 📖	mathematical	—	`diam` `ediam` `Top.top` `ENat` `instTopENat`	—	`not_iff_not` `ediam_ne_top_of_diam_ne_zero` `diam_ne_zero_of_ediam_ne_top`
`diam_eq_zero_of_ediam_eq_top` 📖	mathematical	`ediam` `Top.top` `ENat` `instTopENat`	`diam`	—	`diam.eq_1` `ENat.toNat_top`
`diam_eq_zero_of_not_connected` 📖	mathematical	`Connected`	`diam`	—	`isEmpty_or_nonempty` `diam.eq_1` `ediam.eq_1` `ciSup_of_empty` `bot_eq_zero'` `ediam_eq_top_of_not_connected` `ENat.toNat_top`
`diam_ne_zero_of_ediam_ne_top` 📖	—	—	—	—	`exists_pair_ne` `pos_iff_ne_zero` `Nat.instCanonicallyOrderedAdd` `lt_of_lt_of_le` `Connected.pos_dist_of_ne` `connected_of_ediam_ne_top` `Nontrivial.to_nonempty` `dist_le_diam`
`diam_top` 📖	mathematical	—	`diam` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`diam.eq_1` `ediam_top` `ENat.toNat_one`
`dist_le_diam` 📖	mathematical	—	`dist` `diam`	—	`ENat.toNat_le_toNat` `edist_le_ediam`
`eccent_bot` 📖	mathematical	—	`eccent` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Top.top` `ENat` `instTopENat`	—	`eccent_eq_top_of_not_connected` `not_connected_bot`
`eccent_def` 📖	mathematical	—	`eccent` `iSup` `ENat` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `edist`	—	—
`eccent_eq_one_iff` 📖	mathematical	—	`eccent` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Adj`	—	`ENat.one_le_iff_ne_zero` `eccent_ne_zero` `LE.le.ge_iff_eq'` `eccent_le_one_iff`
`eccent_eq_top_of_not_connected` 📖	mathematical	`Connected`	`eccent` `Top.top` `ENat` `instTopENat`	—	`Mathlib.Tactic.Push.not_forall_eq` `connected_iff_exists_forall_reachable` `eq_top_iff` `edist_eq_top_of_not_reachable` `le_iSup`
`eccent_eq_zero_iff` 📖	mathematical	—	`eccent` `ENat` `instZeroENat`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `eccent_ne_zero` `eccent_eq_zero_of_subsingleton`
`eccent_eq_zero_of_subsingleton` 📖	mathematical	—	`eccent` `ENat` `instZeroENat`	—	`subsingleton_iff`
`eccent_le_ediam` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `eccent` `ediam`	—	`le_iSup`
`eccent_le_iff` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `eccent` `edist`	—	`iSup_le_iff`
`eccent_le_one_iff` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `eccent` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Adj`	—	`LE.le.trans` `edist_le_eccent` `Order.one_le_iff_pos` `IsOrderedRing.toZeroLEOneClass` `NeZero.one` `edist_pos_of_ne` `edist_eq_one_iff_adj` `le_antisymm` `eccent_le_iff` `edist_le_one_iff_adj_or_eq`
`eccent_ne_zero` 📖	—	—	—	—	`exists_ne` `Mathlib.Tactic.Contrapose.contrapose₄`
`eccent_pos_iff` 📖	mathematical	—	`ENat` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `instZeroENat` `eccent` `Nontrivial`	—	`pos_iff_ne_zero` `not_subsingleton_iff_nontrivial` `eccent_eq_zero_iff`
`eccent_top` 📖	mathematical	—	`eccent` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`le_antisymm` `eccent.eq_1` `iSup_le_iff` `eq_or_ne` `edist_self` `edist_top_of_ne` `Order.one_le_iff_pos` `IsOrderedRing.toZeroLEOneClass` `NeZero.one` `pos_iff_ne_zero` `eccent_ne_zero`
`ediam_anti` 📖	mathematical	`SimpleGraph` `instLE`	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `ediam`	—	`iSup₂_mono` `edist_anti`
`ediam_bot` 📖	mathematical	—	`ediam` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Top.top` `ENat` `instTopENat`	—	`ediam_eq_top_of_not_connected` `Nontrivial.to_nonempty` `not_connected_bot`
`ediam_def` 📖	mathematical	—	`ediam` `iSup` `ENat` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `edist`	—	`ediam.eq_1` `eccent_def` `iSup_prod`
`ediam_eq_iSup_iSup_edist` 📖	mathematical	—	`ediam` `iSup` `ENat` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `edist`	—	—
`ediam_eq_one` 📖	mathematical	—	`ediam` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra`	—	`eq_top_iff_forall_eccent_eq_one` `le_antisymm` `eccent_le_ediam` `Order.one_le_iff_pos` `IsOrderedRing.toZeroLEOneClass` `NeZero.one` `pos_iff_ne_zero` `eccent_ne_zero` `ediam_top`
`ediam_eq_top` 📖	mathematical	—	`ediam` `Top.top` `ENat` `instTopENat` `Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `edist`	—	—
`ediam_eq_top_of_not_connected` 📖	mathematical	`Connected`	`ediam` `Top.top` `ENat` `instTopENat`	—	`Mathlib.Tactic.Push.not_forall_eq` `connected_iff_exists_forall_reachable` `eq_top_iff` `edist_eq_top_of_not_reachable` `edist_le_ediam`
`ediam_eq_top_of_not_preconnected` 📖	mathematical	`Preconnected`	`ediam` `Top.top` `ENat` `instTopENat`	—	`isEmpty_or_nonempty` `IsEmpty.forall_iff` `ediam_eq_top_of_not_connected` `connected_iff`
`ediam_eq_zero_iff_subsingleton` 📖	mathematical	—	`ediam` `ENat` `instZeroENat`	—	`subsingleton_of_ediam_eq_zero` `ediam_eq_zero_of_subsingleton`
`ediam_eq_zero_of_subsingleton` 📖	mathematical	—	`ediam` `ENat` `instZeroENat`	—	`ediam_def` `ENat.iSup_eq_zero` `subsingleton_iff`
`ediam_le_iff` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `ediam` `edist`	—	`iSup₂_le_iff`
`ediam_le_of_edist_le` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `edist`	`ediam`	—	`iSup₂_le`
`ediam_le_two_mul_radius` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `ediam` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `instOfNatAtLeastTwo` `ENat.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `radius`	—	`isEmpty_or_nonempty` `Nat.instAtLeastTwoHAddOfNat` `radius_eq_top_of_isEmpty` `le_top` `exists_eccent_eq_radius` `exists_edist_eq_ediam_of_ne_top` `connected_iff_ediam_ne_top` `le_trans` `edist_triangle` `two_mul` `add_le_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `edist_le_eccent` `edist_comm` `radius_eq_top_of_not_connected`
`ediam_ne_top_of_diam_ne_zero` 📖	—	—	—	—	`diam_eq_zero_of_ediam_eq_top`
`ediam_ne_zero` 📖	—	—	—	—	`exists_pair_ne` `Mathlib.Tactic.Contrapose.contrapose₄`
`ediam_ne_zero_iff_nontrivial` 📖	mathematical	—	`Nontrivial`	—	`nontrivial_of_ediam_ne_zero` `ediam_ne_zero`
`ediam_top` 📖	mathematical	—	`ediam` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`eccent_top` `ciSup_const` `Nontrivial.to_nonempty`
`edist_le_eccent` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `edist` `eccent`	—	`le_iSup`
`edist_le_ediam` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `edist` `ediam`	—	`le_iSup₂`
`eq_top_iff_forall_eccent_eq_one` 📖	mathematical	—	`Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `eccent` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`eccent_top` `ext` `Adj.ne` `edist_eq_one_iff_adj` `le_antisymm` `edist_le_eccent` `Order.one_le_iff_pos` `IsOrderedRing.toZeroLEOneClass` `NeZero.one` `pos_iff_ne_zero` `Iff.ne` `edist_eq_zero_iff`
`exists_dist_eq_diam` 📖	mathematical	—	`dist` `diam`	—	`exists_edist_eq_ediam_of_ne_top` `ediam_ne_top_of_diam_ne_zero` `diam.eq_1` `dist.eq_1`
`exists_eccent_eq_ediam_of_finite` 📖	mathematical	—	`eccent` `ediam`	—	`exists_eq_ciSup_of_finite`
`exists_eccent_eq_ediam_of_ne_top` 📖	mathematical	—	`eccent` `ediam`	—	`ENat.exists_eq_iSup_of_lt_top` `Ne.lt_top`
`exists_eccent_eq_radius` 📖	mathematical	—	`eccent` `radius`	—	`ENat.exists_eq_iInf`
`exists_edist_eq_eccent_of_finite` 📖	mathematical	—	`edist` `eccent`	—	`exists_eq_ciSup_of_finite`
`exists_edist_eq_ediam_of_finite` 📖	mathematical	—	`edist` `ediam`	—	`Prod.exists'` `exists_eq_ciSup_of_finite` `Finite.instProd` `ediam_def`
`exists_edist_eq_ediam_of_ne_top` 📖	mathematical	—	`edist` `ediam`	—	`ENat.exists_eq_iSup₂_of_lt_top` `Ne.lt_top`
`exists_edist_eq_radius_of_finite` 📖	mathematical	—	`edist` `radius`	—	`exists_eccent_eq_radius` `exists_edist_eq_eccent_of_finite`
`mem_center_iff` 📖	mathematical	—	`Set` `Set.instMembership` `center` `eccent` `radius`	—	—
`nontrivial_of_diam_ne_zero` 📖	mathematical	—	`Nontrivial`	—	`Mathlib.Tactic.Contrapose.contrapose₂`
`nontrivial_of_ediam_ne_zero` 📖	mathematical	—	`Nontrivial`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `ediam_eq_zero_of_subsingleton`
`preconnected_of_ediam_ne_top` 📖	mathematical	—	`Preconnected`	—	`Not.imp_symm` `ediam_eq_top_of_not_preconnected`
`radius_bot` 📖	mathematical	—	`radius` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Top.top` `ENat` `instTopENat`	—	`radius_eq_top_of_not_connected` `not_connected_bot`
`radius_eq_ediam_iff` 📖	mathematical	—	`radius` `ediam` `eccent`	—	`le_antisymm` `eccent_le_ediam` `radius_le_eccent` `iSup_le` `Eq.le` `le_iInf` `Eq.ge`
`radius_eq_iInf_iSup_edist` 📖	mathematical	—	`radius` `iInf` `ENat` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `edist`	—	—
`radius_eq_top_of_isEmpty` 📖	mathematical	—	`radius` `Top.top` `ENat` `instTopENat`	—	`iInf_of_empty`
`radius_eq_top_of_not_connected` 📖	mathematical	`Connected`	`radius` `Top.top` `ENat` `instTopENat`	—	`eccent_eq_top_of_not_connected` `iInf_top`
`radius_eq_zero_iff` 📖	mathematical	—	`radius` `ENat` `instZeroENat`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `radius.eq_1` `ENat.iInf_eq_zero`
`radius_le_eccent` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `radius` `eccent`	—	`iInf_le`
`radius_le_ediam` 📖	mathematical	—	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instCompleteLinearOrderENat` `radius` `ediam`	—	`iInf_le_iSup`
`radius_ne_top_iff` 📖	mathematical	—	`Connected`	—	`Not.imp_symm` `radius_eq_top_of_not_connected` `exists_edist_eq_radius_of_finite` `edist_ne_top_iff_reachable` `Connected.preconnected`
`radius_ne_zero_of_nontrivial` 📖	—	—	—	—	`ENat.one_le_iff_ne_zero` `le_iInf` `eccent_ne_zero`
`radius_top` 📖	mathematical	—	`radius` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `ENat` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	—	`eccent_top` `ciInf_const` `Nontrivial.to_nonempty`
`subsingleton_of_ediam_eq_zero` 📖	—	`ediam` `ENat` `instZeroENat`	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `ediam_ne_zero`

---

← Back to Index