Commit 2022-12-15 21:06 c4552925

View on Github →

feat: port Order.Bounds.Basic (#1040) aba57d4d3dae35460225919dcd82fe91355162f9

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Bounds/Basic.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.dual

added theorem BddAbove.exists_ge

added theorem BddAbove.image2

added theorem BddAbove.image2_bddBelow

added theorem BddAbove.insert

added theorem BddAbove.inter_of_left

added theorem BddAbove.inter_of_right

added theorem BddAbove.mono

added theorem BddAbove.union

added def BddAbove

added theorem BddBelow.bddAbove_image2_of_bddAbove

added theorem BddBelow.bddBelow_image2_of_bddAbove

added theorem BddBelow.dual

added theorem BddBelow.exists_le

added theorem BddBelow.image2

added theorem BddBelow.image2_bddAbove

added theorem BddBelow.insert

added theorem BddBelow.inter_of_left

added theorem BddBelow.inter_of_right

added theorem BddBelow.mono

added theorem BddBelow.union

added def BddBelow

added theorem IsGLB.bddBelow

added theorem IsGLB.dual

added theorem IsGLB.exists_between'

added theorem IsGLB.exists_between

added theorem IsGLB.insert

added theorem IsGLB.inter_Iic_of_mem

added theorem IsGLB.lowerBounds_eq

added theorem IsGLB.mono

added theorem IsGLB.nonempty

added theorem IsGLB.of_image

added theorem IsGLB.of_subset_of_superset

added theorem IsGLB.union

added theorem IsGLB.unique

added def IsGLB

added theorem IsGreatest.bddAbove

added theorem IsGreatest.dual

added theorem IsGreatest.image2

added theorem IsGreatest.insert

added theorem IsGreatest.isGreatest_iff_eq

added theorem IsGreatest.isGreatest_image2_of_isLeast

added theorem IsGreatest.isLUB

added theorem IsGreatest.isLeast_image2

added theorem IsGreatest.isLeast_image2_of_isLeast

added theorem IsGreatest.mono

added theorem IsGreatest.nonempty

added def IsGreatest.orderTop

added theorem IsGreatest.union

added theorem IsGreatest.unique

added theorem IsGreatest.upperBounds_eq

added def IsGreatest

added theorem IsLUB.bddAbove

added theorem IsLUB.dual

added theorem IsLUB.exists_between'

added theorem IsLUB.exists_between

added theorem IsLUB.insert

added theorem IsLUB.inter_Ici_of_mem

added theorem IsLUB.mono

added theorem IsLUB.nonempty

added theorem IsLUB.of_image

added theorem IsLUB.of_subset_of_superset

added theorem IsLUB.union

added theorem IsLUB.unique

added theorem IsLUB.upperBounds_eq

added def IsLUB

added theorem IsLeast.bddBelow

added theorem IsLeast.dual

added theorem IsLeast.image2

added theorem IsLeast.insert

added theorem IsLeast.isGLB

added theorem IsLeast.isGreatest_image2

added theorem IsLeast.isGreatest_image2_of_isGreatest

added theorem IsLeast.isLeast_iff_eq

added theorem IsLeast.isLeast_image2_of_isGreatest

added theorem IsLeast.lowerBounds_eq

added theorem IsLeast.mono

added theorem IsLeast.nonempty

added def IsLeast.orderBot

added theorem IsLeast.union

added theorem IsLeast.unique

added def IsLeast

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 NoMaxOrder.upperBounds_univ

added theorem NoMinOrder.lowerBounds_univ

added theorem OrderBot.lowerBounds_univ

added theorem OrderTop.upperBounds_univ

added theorem Set.Nonempty.bddAbove_lowerBounds

added theorem Set.Nonempty.bddBelow_upperBounds

added theorem Set.subsingleton_of_isLUB_le_isGLB

added theorem bddAbove_Icc

added theorem bddAbove_Ico

added theorem bddAbove_Iic

added theorem bddAbove_Iio

added theorem bddAbove_Ioc

added theorem bddAbove_Ioo

added theorem bddAbove_def

added theorem bddAbove_empty

added theorem bddAbove_iff_exists_ge

added theorem bddAbove_iff_subset_Iic

added theorem bddAbove_insert

added theorem bddAbove_singleton

added theorem bddAbove_union

added theorem bddBelow_Icc

added theorem bddBelow_Ici

added theorem bddBelow_Ico

added theorem bddBelow_Ioc

added theorem bddBelow_Ioi

added theorem bddBelow_Ioo

added theorem bddBelow_bddAbove_iff_subset_Icc

added theorem bddBelow_def

added theorem bddBelow_empty

added theorem bddBelow_iff_exists_le

added theorem bddBelow_iff_subset_Ici

added theorem bddBelow_insert

added theorem bddBelow_singleton

added theorem bddBelow_union

added theorem bot_mem_lowerBounds

added theorem exists_glb_Ioi

added theorem exists_lub_Iio

added theorem glb_Ioi_eq_self_or_Ioi_eq_Ici

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_Ici

added theorem isGLB_Ioi

added theorem isGLB_empty

added theorem isGLB_iff_le_iff

added theorem isGLB_le_isLUB

added theorem isGLB_lt_iff

added theorem isGLB_lt_isLUB_of_ne

added theorem isGLB_pair

added theorem isGLB_pi

added theorem isGLB_prod

added theorem isGLB_singleton

added theorem isGLB_upperBounds

added theorem isGreatest_Icc

added theorem isGreatest_Iic

added theorem isGreatest_Ioc

added theorem isGreatest_pair

added theorem isGreatest_singleton

added theorem isGreatest_top_iff

added theorem isGreatest_union_iff

added theorem isGreatest_univ

added theorem isLUB_Icc

added theorem isLUB_Ico

added theorem isLUB_Iic

added theorem isLUB_Iio

added theorem isLUB_Ioc

added theorem isLUB_Ioo

added theorem isLUB_empty

added theorem isLUB_iff_le_iff

added theorem isLUB_le_iff

added theorem isLUB_lowerBounds

added theorem isLUB_lt_iff

added theorem isLUB_pair

added theorem isLUB_pi

added theorem isLUB_prod

added theorem isLUB_singleton

added theorem isLUB_univ

added theorem isLeast_Icc

added theorem isLeast_Ici

added theorem isLeast_Ico

added theorem isLeast_bot_iff

added theorem isLeast_pair

added theorem isLeast_singleton

added theorem isLeast_union_iff

added theorem isLeast_univ

added theorem is_glb_Icc

added theorem is_glb_Ico

added theorem is_glb_Ioc

added theorem is_glb_Ioo

added theorem is_glb_univ

added theorem le_glb_Ioi

added theorem le_isGLB_iff

added theorem le_of_isLUB_le_isGLB

added def lowerBounds

added theorem lowerBounds_Icc

added theorem lowerBounds_Ici

added theorem lowerBounds_Ico

added theorem lowerBounds_Ioc

added theorem lowerBounds_Ioi

added theorem lowerBounds_Ioo

added theorem lowerBounds_empty

added theorem lowerBounds_insert

added theorem lowerBounds_le_upperBounds

added theorem lowerBounds_mono

added theorem lowerBounds_mono_mem

added theorem lowerBounds_mono_set

added theorem lowerBounds_singleton

added theorem lowerBounds_union

added theorem lt_isGLB_iff

added theorem lt_isLUB_iff

added theorem lub_Iio_eq_self_or_Iio_eq_Iic

added theorem lub_Iio_le

added theorem mem_lowerBounds

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

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

added theorem nonempty_of_not_bddAbove

added theorem nonempty_of_not_bddBelow

added theorem not_bddAbove_iff'

added theorem not_bddAbove_iff

added theorem not_bddAbove_univ

added theorem not_bddBelow_iff'

added theorem not_bddBelow_iff

added theorem not_bddBelow_univ

added theorem subset_lowerBounds_upperBounds

added theorem subset_upperBounds_lowerBounds

added theorem top_mem_upperBounds

added theorem union_lowerBounds_subset_lowerBounds_inter

added theorem union_upperBounds_subset_upperBounds_inter

added def upperBounds

added theorem upperBounds_Icc

added theorem upperBounds_Ico

added theorem upperBounds_Iic

added theorem upperBounds_Iio

added theorem upperBounds_Ioc

added theorem upperBounds_Ioo

added theorem upperBounds_empty

added theorem upperBounds_insert

added theorem upperBounds_mono

added theorem upperBounds_mono_mem

added theorem upperBounds_mono_set

added theorem upperBounds_singleton

added theorem upperBounds_union