Commit 2024-10-19 16:03 64ac27ea

View on Github →

chore(Order/Bounds/Basic): Split long file into two shorter files (#16539) This PR transfers some of the content from Order/Bounds/Basic into a new file, Order/Bounds/Image.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Bounds/Basic.lean

deleted theorem Antitone.image_lowerBounds_subset_upperBounds_image

deleted theorem Antitone.image_upperBounds_subset_lowerBounds_image

deleted theorem Antitone.map_bddAbove

deleted theorem Antitone.map_bddBelow

deleted theorem Antitone.map_isGreatest

deleted theorem Antitone.map_isLeast

deleted theorem Antitone.mem_lowerBounds_image

deleted theorem Antitone.mem_upperBounds_image

deleted theorem AntitoneOn.image_lowerBounds_subset_upperBounds_image

deleted theorem AntitoneOn.image_upperBounds_subset_lowerBounds_image

deleted theorem AntitoneOn.map_bddAbove

deleted theorem AntitoneOn.map_bddBelow

deleted theorem AntitoneOn.map_isGreatest

deleted theorem AntitoneOn.map_isLeast

deleted theorem AntitoneOn.mem_lowerBounds_image

deleted theorem AntitoneOn.mem_lowerBounds_image_self

deleted theorem AntitoneOn.mem_upperBounds_image

deleted theorem AntitoneOn.mem_upperBounds_image_self

deleted theorem BddAbove.bddAbove_image2_of_bddBelow

deleted theorem BddAbove.bddBelow_image2_of_bddAbove

deleted theorem BddAbove.image2_bddBelow

deleted theorem BddAbove.range_comp

deleted theorem BddAbove.range_mono

deleted theorem BddBelow.bddAbove_image2_of_bddAbove

deleted theorem BddBelow.bddBelow_image2_of_bddAbove

deleted theorem BddBelow.image2_bddAbove

deleted theorem BddBelow.range_comp

deleted theorem BddBelow.range_mono

deleted theorem IsGLB.of_image

deleted theorem IsGreatest.isGreatest_image2_of_isLeast

deleted theorem IsGreatest.isLeast_image2

deleted theorem IsGreatest.isLeast_image2_of_isLeast

deleted theorem IsLUB.of_image

deleted theorem IsLeast.isGreatest_image2

deleted theorem IsLeast.isGreatest_image2_of_isGreatest

deleted theorem IsLeast.isLeast_image2_of_isGreatest

deleted theorem Monotone.image_lowerBounds_subset_lowerBounds_image

deleted theorem Monotone.image_upperBounds_subset_upperBounds_image

deleted theorem Monotone.map_bddAbove

deleted theorem Monotone.map_bddBelow

deleted theorem Monotone.map_isGreatest

deleted theorem Monotone.map_isLeast

deleted theorem Monotone.mem_lowerBounds_image

deleted theorem Monotone.mem_upperBounds_image

deleted theorem MonotoneOn.image_lowerBounds_subset_lowerBounds_image

deleted theorem MonotoneOn.image_upperBounds_subset_upperBounds_image

deleted theorem MonotoneOn.map_bddAbove

deleted theorem MonotoneOn.map_bddBelow

deleted theorem MonotoneOn.map_isGreatest

deleted theorem MonotoneOn.map_isLeast

deleted theorem MonotoneOn.mem_lowerBounds_image

deleted theorem MonotoneOn.mem_lowerBounds_image_self

deleted theorem MonotoneOn.mem_upperBounds_image

deleted theorem MonotoneOn.mem_upperBounds_image_self

deleted theorem bddAbove_pi

deleted theorem bddAbove_prod

deleted theorem bddAbove_range_pi

deleted theorem bddAbove_range_prod

deleted theorem bddBelow_pi

deleted theorem bddBelow_prod

deleted theorem bddBelow_range_pi

deleted theorem bddBelow_range_prod

deleted theorem image2_lowerBounds_lowerBounds_subset

deleted theorem image2_lowerBounds_lowerBounds_subset_lowerBounds_image2

deleted theorem image2_lowerBounds_upperBounds_subset_lowerBounds_image2

deleted theorem image2_lowerBounds_upperBounds_subset_upperBounds_image2

deleted theorem image2_upperBounds_lowerBounds_subset_lowerBounds_image2

deleted theorem image2_upperBounds_lowerBounds_subset_upperBounds_image2

deleted theorem image2_upperBounds_upperBounds_subset

deleted theorem image2_upperBounds_upperBounds_subset_upperBounds_image2

deleted theorem isGLB_pi

deleted theorem isGLB_prod

deleted theorem isLUB_pi

deleted theorem isLUB_prod

deleted theorem mem_lowerBounds_image2

deleted theorem mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds

deleted theorem mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds

deleted theorem mem_lowerBounds_image2_of_mem_upperBounds

deleted theorem mem_upperBounds_image2

deleted theorem mem_upperBounds_image2_of_mem_lowerBounds

deleted theorem mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds

deleted theorem mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds

Created Mathlib/Order/Bounds/Image.lean

added theorem Antitone.image_lowerBounds_subset_upperBounds_image

added theorem Antitone.image_upperBounds_subset_lowerBounds_image

added theorem Antitone.map_bddAbove

added theorem Antitone.map_bddBelow

added theorem Antitone.map_isGreatest

added theorem Antitone.map_isLeast

added theorem Antitone.mem_lowerBounds_image

added theorem Antitone.mem_upperBounds_image

added theorem AntitoneOn.image_lowerBounds_subset_upperBounds_image

added theorem AntitoneOn.image_upperBounds_subset_lowerBounds_image

added theorem AntitoneOn.map_bddAbove

added theorem AntitoneOn.map_bddBelow

added theorem AntitoneOn.map_isGreatest

added theorem AntitoneOn.map_isLeast

added theorem AntitoneOn.mem_lowerBounds_image

added theorem AntitoneOn.mem_lowerBounds_image_self

added theorem AntitoneOn.mem_upperBounds_image

added theorem AntitoneOn.mem_upperBounds_image_self

added theorem BddAbove.bddAbove_image2_of_bddBelow

added theorem BddAbove.bddBelow_image2_of_bddAbove

added theorem BddAbove.image2_bddBelow

added theorem BddAbove.range_comp

added theorem BddAbove.range_mono

added theorem BddBelow.bddAbove_image2_of_bddAbove

added theorem BddBelow.bddBelow_image2_of_bddAbove

added theorem BddBelow.image2_bddAbove

added theorem BddBelow.range_comp

added theorem BddBelow.range_mono

added theorem IsGLB.of_image

added theorem IsGreatest.isGreatest_image2_of_isLeast

added theorem IsGreatest.isLeast_image2

added theorem IsGreatest.isLeast_image2_of_isLeast

added theorem IsLUB.of_image

added theorem IsLeast.isGreatest_image2

added theorem IsLeast.isGreatest_image2_of_isGreatest

added theorem IsLeast.isLeast_image2_of_isGreatest

added theorem Monotone.image_lowerBounds_subset_lowerBounds_image

added theorem Monotone.image_upperBounds_subset_upperBounds_image

added theorem Monotone.map_bddAbove

added theorem Monotone.map_bddBelow

added theorem Monotone.map_isGreatest

added theorem Monotone.map_isLeast

added theorem Monotone.mem_lowerBounds_image

added theorem Monotone.mem_upperBounds_image

added theorem MonotoneOn.image_lowerBounds_subset_lowerBounds_image

added theorem MonotoneOn.image_upperBounds_subset_upperBounds_image

added theorem MonotoneOn.map_bddAbove

added theorem MonotoneOn.map_bddBelow

added theorem MonotoneOn.map_isGreatest

added theorem MonotoneOn.map_isLeast

added theorem MonotoneOn.mem_lowerBounds_image

added theorem MonotoneOn.mem_lowerBounds_image_self

added theorem MonotoneOn.mem_upperBounds_image

added theorem MonotoneOn.mem_upperBounds_image_self

added theorem bddAbove_pi

added theorem bddAbove_prod

added theorem bddAbove_range_pi

added theorem bddAbove_range_prod

added theorem bddBelow_pi

added theorem bddBelow_prod

added theorem bddBelow_range_pi

added theorem bddBelow_range_prod

added theorem image2_lowerBounds_lowerBounds_subset

added theorem image2_lowerBounds_lowerBounds_subset_lowerBounds_image2

added theorem image2_lowerBounds_upperBounds_subset_lowerBounds_image2

added theorem image2_lowerBounds_upperBounds_subset_upperBounds_image2

added theorem image2_upperBounds_lowerBounds_subset_lowerBounds_image2

added theorem image2_upperBounds_lowerBounds_subset_upperBounds_image2

added theorem image2_upperBounds_upperBounds_subset

added theorem image2_upperBounds_upperBounds_subset_upperBounds_image2

added theorem isGLB_pi

added theorem isGLB_prod

added theorem isLUB_pi

added theorem isLUB_prod

added theorem mem_lowerBounds_image2

added theorem mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds

added theorem mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_upperBounds

added theorem mem_lowerBounds_image2_of_mem_upperBounds

added theorem mem_upperBounds_image2

added theorem mem_upperBounds_image2_of_mem_lowerBounds

added theorem mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds

added theorem mem_upperBounds_image2_of_mem_upperBounds_of_mem_upperBounds

Modified Mathlib/Order/Bounds/OrderIso.lean

Modified Mathlib/Order/CompleteLattice.lean

Modified Mathlib/Order/GaloisConnection.lean