module module

`IndisputableMonolith.Mathematics.DistanceShellMultiplicity`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Mathematics.BipartiteDistanceSpectrum module_import

declarations in this module (337)

abbrev Point2 L26
def orderedPairEvents L29
def orderedDistanceSpectrum L34
def orderedShellMultiplicity L39
def SparseShell L46
def IsDiameterShell L50
theorem diameter_shell_nonneg L56
theorem isDiameterShell_unique L66
theorem dist_le_of_diameter_shell L74
def Erdos132Ordered L95
def SparseShellsDiverge L104
def SecondSparseShellFluxBridge L118
def HopfPannwitzOrderedDiameterBound L129
def DiameterShellExistsEventually L139
def DiameterShellSparseBound L147
def diameterOrderedEdges L154
theorem orderedShellMultiplicity_eq_diameterOrderedEdges_card L161
theorem diameter_ordered_edge_data L168
theorem diameter_ordered_edges_cross_distances_le L181
def DiameterShellOrderedMultiplicityBound L201
theorem diameter_shell_sparse_from_ordered_bound L210
def OnClosedSegment L218
theorem left_endpoint_on_segment L222
theorem right_endpoint_on_segment L228
theorem on_closed_segment_symm L234
theorem on_closed_segment_comm L243
theorem midpoint_on_closed_segment L248
theorem on_closed_segment_convex L255
theorem on_closed_segment_self_eq L269
theorem dist_add_on_closed_segment L278
theorem dist_left_le_of_on_closed_segment L290
theorem dist_right_le_of_on_closed_segment L298
theorem eq_right_of_on_closed_segment_of_dist_left_eq L306
theorem eq_left_of_on_closed_segment_of_dist_right_eq L315
theorem onClosedSegment_iff_mem_segment L325
theorem on_closed_segment_strict L340
def OrderedEdgesMeetGeometrically L361
def OrderedEdgesGeometricallyDisjoint L369
theorem ordered_edges_meet_symm L374
theorem ordered_edges_meet_comm L381
theorem ordered_edges_meet_swap_left L387
theorem ordered_edges_meet_swap_right L395
theorem ordered_edges_meet_of_fst_on_segment L404
theorem ordered_edges_meet_of_snd_on_segment L411
theorem ordered_edges_meet_of_fst_on_segment_symm L418
theorem ordered_edges_meet_of_snd_on_segment_symm L425
def OrderedEdgesShareEndpoint L432
theorem ordered_edges_meet_of_share_endpoint L437
def NoDisjointDiameterEdges L457
def DiameterSegmentsMeetLocally L470
def EndpointDisjointDiameterSegmentsMeetLocally L482
theorem diameter_segments_meet_from_endpoint_disjoint_core L495
def FourPointDiameterCrossing L508
theorem four_point_diameter_crossing_zero_case L521
def orient2 L536
theorem orient2_swap L540
theorem orient2_cyclic L558
theorem orient2_cyclic' L564
theorem orient2_plucker L570
theorem orient2_bcd_decomposition L576
theorem orient2_alternating_sum_eq_zero L583
theorem orient2_zero_transitive L592
theorem orient2_zero_transitive_swap L627
theorem orient2_zero_of_two_points_on_line_and_point_on_join L635
theorem orient2_left_self L663
theorem orient2_right_self L669
theorem orient2_eq_zero_of_on_closed_segment L676
theorem orient2_affine_third L686
theorem orient2_of_on_closed_segment L696
theorem exists_scalar_of_orient2_zero L708
theorem dist_from_diff_eq_smul L738
theorem affine_zero_of_nonpos_nonneg L764
theorem exists_orient2_zero_on_segment_of_nonpos_nonneg L790
theorem exists_orient2_zero_on_segment_of_nonneg_nonpos L802
theorem same_strict_sign_of_pos_mul L812
theorem convex_combo_ne_zero_of_same_strict_sign L837
theorem same_side_segments_disjoint L882
def ProperSegmentSeparation L901
theorem proper_segment_separation_signs L907
theorem proper_segment_separation_geometrically_disjoint L919

… and 257 more