Commit 2023-02-05 17:41 9fd022a7

View on Github →

feat: port Topology.Order.Basic (#2052)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Set/Countable.lean

added theorem Set.Countable.of_diff

Modified Mathlib/Order/Cover.lean

added theorem LT.lt.exists_disjoint_Iio_Ioi

Modified Mathlib/Topology/ContinuousOn.lean

added theorem nhdsWithin_inter_of_mem'

Created Mathlib/Topology/Order/Basic.lean

added theorem Antitone.map_cinfᵢ_of_continuousAt

added theorem Antitone.map_cinfₛ_of_continuousAt

added theorem Antitone.map_csupr_of_continuousAt

added theorem Antitone.map_csupₛ_of_continuousAt

added theorem Antitone.map_infᵢ_of_continuousAt'

added theorem Antitone.map_infᵢ_of_continuousAt

added theorem Antitone.map_infₛ_of_continuousAt'

added theorem Antitone.map_infₛ_of_continuousAt

added theorem Antitone.map_supᵢ_of_continuousAt'

added theorem Antitone.map_supᵢ_of_continuousAt

added theorem Antitone.map_supₛ_of_continuousAt'

added theorem Antitone.map_supₛ_of_continuousAt

added theorem Continuous.bddAbove_range_of_hasCompactMulSupport

added theorem Continuous.bddBelow_range_of_hasCompactMulSupport

added theorem Continuous.if_le

added theorem ContinuousWithinAt.closure_le

added theorem Dense.exists_between

added theorem Dense.exists_countable_dense_subset_no_bot_top

added theorem Dense.exists_ge'

added theorem Dense.exists_le'

added theorem Dense.orderDual

added theorem Filter.Eventually.exists_Ioo_subset

added theorem Filter.Eventually.exists_gt

added theorem Filter.Eventually.exists_lt

added theorem Filter.Tendsto.add_atBot

added theorem Filter.Tendsto.add_atTop

added theorem Filter.Tendsto.atBot_add

added theorem Filter.Tendsto.atTop_add

added theorem Filter.Tendsto.eventually_lt

added theorem Filter.Tendsto.min_left

added theorem Filter.Tendsto.min_right

added theorem Filter.map_neg_eq_comap_neg

added theorem Filter.tendsto_nhds_max_left

added theorem Filter.tendsto_nhds_max_right

added theorem Filter.tendsto_nhds_min_left

added theorem Filter.tendsto_nhds_min_right

added theorem Icc_mem_nhds

added theorem Icc_mem_nhdsWithin_Ici'

added theorem Icc_mem_nhdsWithin_Ici

added theorem Icc_mem_nhdsWithin_Iic'

added theorem Icc_mem_nhdsWithin_Iic

added theorem Icc_mem_nhdsWithin_Iio'

added theorem Icc_mem_nhdsWithin_Iio

added theorem Icc_mem_nhdsWithin_Ioi'

added theorem Icc_mem_nhdsWithin_Ioi

added theorem Ici_mem_nhds

added theorem Ico_mem_nhds

added theorem Ico_mem_nhdsWithin_Ici'

added theorem Ico_mem_nhdsWithin_Ici

added theorem Ico_mem_nhdsWithin_Iic

added theorem Ico_mem_nhdsWithin_Iio'

added theorem Ico_mem_nhdsWithin_Iio

added theorem Ico_mem_nhdsWithin_Ioi'

added theorem Ico_mem_nhdsWithin_Ioi

added theorem Ico_subset_closure_interior

added theorem Iic_mem_nhds

added theorem Iio_mem_nhds

added theorem Ioc_mem_nhds

added theorem Ioc_mem_nhdsWithin_Ici

added theorem Ioc_mem_nhdsWithin_Iic'

added theorem Ioc_mem_nhdsWithin_Iic

added theorem Ioc_mem_nhdsWithin_Iio'

added theorem Ioc_mem_nhdsWithin_Iio

added theorem Ioc_mem_nhdsWithin_Ioi'

added theorem Ioc_mem_nhdsWithin_Ioi

added theorem Ioc_subset_closure_interior

added theorem Ioi_mem_nhds

added theorem Ioo_mem_nhds

added theorem Ioo_mem_nhdsWithin_Ici

added theorem Ioo_mem_nhdsWithin_Iic

added theorem Ioo_mem_nhdsWithin_Iio'

added theorem Ioo_mem_nhdsWithin_Iio

added theorem Ioo_mem_nhdsWithin_Ioi'

added theorem Ioo_mem_nhdsWithin_Ioi

added theorem Ioo_subset_closure_interior

added theorem IsClosed.cinfₛ_mem

added theorem IsClosed.csupₛ_mem

added theorem IsClosed.epigraph

added theorem IsClosed.hypograph

added theorem IsClosed.infₛ_mem

added theorem IsClosed.isClosed_le

added theorem IsClosed.supₛ_mem

added theorem IsCompact.bddAbove

added theorem IsCompact.bddAbove_image

added theorem IsCompact.bddBelow

added theorem IsCompact.bddBelow_image

added theorem IsGLB.exists_seq_antitone_tendsto

added theorem IsGLB.exists_seq_strictAnti_tendsto_of_not_mem

added theorem IsGLB.frequently_mem

added theorem IsGLB.frequently_nhds_mem

added theorem IsGLB.isGLB_of_tendsto

added theorem IsGLB.isLUB_of_tendsto

added theorem IsGLB.mem_closure

added theorem IsGLB.mem_lowerBounds_of_tendsto

added theorem IsGLB.mem_of_isClosed

added theorem IsGLB.mem_upperBounds_of_tendsto

added theorem IsGLB.nhdsWithin_neBot

added theorem IsLUB.exists_seq_monotone_tendsto

added theorem IsLUB.exists_seq_strictMono_tendsto_of_not_mem

added theorem IsLUB.frequently_mem

added theorem IsLUB.frequently_nhds_mem

added theorem IsLUB.isGLB_of_tendsto

added theorem IsLUB.isLUB_of_tendsto

added theorem IsLUB.mem_closure

added theorem IsLUB.mem_lowerBounds_of_tendsto

added theorem IsLUB.mem_of_isClosed

added theorem IsLUB.mem_upperBounds_of_tendsto

added theorem IsLUB.nhdsWithin_neBot

added theorem IsOpen.exists_Ioo_subset

added theorem LinearOrderedAddCommGroup.tendsto_nhds

added theorem Monotone.map_cinfᵢ_of_continuousAt

added theorem Monotone.map_cinfₛ_of_continuousAt

added theorem Monotone.map_csupr_of_continuousAt

added theorem Monotone.map_csupₛ_of_continuousAt

added theorem Monotone.map_infᵢ_of_continuousAt'

added theorem Monotone.map_infᵢ_of_continuousAt

added theorem Monotone.map_infₛ_of_continuousAt'

added theorem Monotone.map_infₛ_of_continuousAt

added theorem Monotone.map_supᵢ_of_continuousAt'

added theorem Monotone.map_supᵢ_of_continuousAt

added theorem Monotone.map_supₛ_of_continuousAt'

added theorem Monotone.map_supₛ_of_continuousAt

added theorem Monotone.tendsto_nhdsWithin_Iio

added theorem Monotone.tendsto_nhdsWithin_Ioi

added def Preorder.topology

added theorem Set.PairwiseDisjoint.countable_of_Ioo

added theorem TFAE_mem_nhdsWithin_Ici

added theorem TFAE_mem_nhdsWithin_Iic

added theorem TFAE_mem_nhdsWithin_Iio

added theorem TFAE_mem_nhdsWithin_Ioi

added theorem cinfₛ_mem_closure

added theorem closure_Icc

added theorem closure_Ici

added theorem closure_Ico

added theorem closure_Iic

added theorem closure_Iio'

added theorem closure_Iio

added theorem closure_Ioc

added theorem closure_Ioi'

added theorem closure_Ioi

added theorem closure_Ioo

added theorem closure_interior_Icc

added theorem closure_le_eq

added theorem closure_lt_subset_le

added theorem comap_coe_Iio_nhdsWithin_Iio

added theorem comap_coe_Ioi_nhdsWithin_Ioi

added theorem comap_coe_Ioo_nhdsWithin_Iio

added theorem comap_coe_Ioo_nhdsWithin_Ioi

added theorem comap_coe_nhdsWithin_Iio_of_Ioo_subset

added theorem comap_coe_nhdsWithin_Ioi_of_Ioo_subset

added theorem continuousWithinAt_Icc_iff_Ici

added theorem continuousWithinAt_Icc_iff_Iic

added theorem continuousWithinAt_Ico_iff_Ici

added theorem continuousWithinAt_Ico_iff_Iio

added theorem continuousWithinAt_Ioc_iff_Iic

added theorem continuousWithinAt_Ioc_iff_Ioi

added theorem continuousWithinAt_Ioo_iff_Iio

added theorem continuousWithinAt_Ioo_iff_Ioi

added theorem continuous_if_le

added theorem continuous_max

added theorem continuous_min

added theorem countable_of_isolated_left'

added theorem countable_of_isolated_right'

added theorem countable_setOf_covby_left

added theorem countable_setOf_covby_right

added theorem csupₛ_mem_closure

added theorem dense_iff_exists_between

added theorem dense_of_exists_between

added theorem disjoint_nhds_atBot

added theorem disjoint_nhds_atTop

added theorem eventually_abs_sub_lt

added theorem eventually_ge_nhds

added theorem eventually_ge_of_tendsto_gt

added theorem eventually_gt_nhds

added theorem eventually_gt_of_tendsto_gt

added theorem eventually_le_nhds

added theorem eventually_le_of_tendsto_lt

added theorem eventually_lt_nhds

added theorem eventually_lt_of_tendsto_lt

added theorem eventually_nhdsWithin_pos_mem_Ioc

added theorem eventually_nhdsWithin_pos_mem_Ioo

added theorem exists_Icc_mem_subset_of_mem_nhds

added theorem exists_Icc_mem_subset_of_mem_nhdsWithin_Ici

added theorem exists_Icc_mem_subset_of_mem_nhdsWithin_Iic

added theorem exists_Ico_subset_of_mem_nhds'

added theorem exists_Ico_subset_of_mem_nhds

added theorem exists_Ioc_subset_of_mem_nhds'

added theorem exists_Ioc_subset_of_mem_nhds

added theorem exists_countable_dense_no_bot_top

added theorem exists_seq_strictAnti_strictMono_tendsto

added theorem exists_seq_strictAnti_tendsto'

added theorem exists_seq_strictAnti_tendsto

added theorem exists_seq_strictAnti_tendsto_nhdsWithin

added theorem exists_seq_strictMono_tendsto'

added theorem exists_seq_strictMono_tendsto

added theorem exists_seq_strictMono_tendsto_nhdsWithin

added theorem exists_seq_tendsto_infₛ

added theorem exists_seq_tendsto_supₛ

added theorem frontier_Icc

added theorem frontier_Ici'

added theorem frontier_Ici

added theorem frontier_Ici_subset

added theorem frontier_Ico

added theorem frontier_Iic'

added theorem frontier_Iic

added theorem frontier_Iic_subset

added theorem frontier_Iio'

added theorem frontier_Iio

added theorem frontier_Ioc

added theorem frontier_Ioi'

added theorem frontier_Ioi

added theorem frontier_Ioo

added theorem frontier_le_subset_eq

added theorem frontier_lt_subset_eq

added theorem ge_mem_nhds

added theorem ge_of_tendsto'

added theorem ge_of_tendsto

added theorem gt_mem_nhds

added theorem induced_orderTopology'

added theorem induced_orderTopology

added theorem induced_topology_eq_preorder

added theorem induced_topology_le_preorder

added theorem inf_nhds_atBot

added theorem inf_nhds_atTop

added theorem infₛ_mem_closure

added theorem interior_Icc

added theorem interior_Ici'

added theorem interior_Ici

added theorem interior_Ico

added theorem interior_Iic'

added theorem interior_Iic

added theorem interior_Iio

added theorem interior_Ioc

added theorem interior_Ioi

added theorem interior_Ioo

added theorem isClosed_Icc

added theorem isClosed_Ici

added theorem isClosed_Iic

added theorem isClosed_ge'

added theorem isClosed_le'

added theorem isClosed_le

added theorem isClosed_le_prod

added theorem isGLB_of_mem_closure

added theorem isGLB_of_mem_nhds

added theorem isLUB_of_mem_closure

added theorem isLUB_of_mem_nhds

added theorem isOpen_Iio

added theorem isOpen_Ioi

added theorem isOpen_Ioo

added theorem isOpen_gt'

added theorem isOpen_iff_generate_intervals

added theorem isOpen_lt'

added theorem isOpen_lt

added theorem isOpen_lt_prod

added theorem le_mem_nhds

added theorem le_of_tendsto'

added theorem le_of_tendsto

added theorem le_of_tendsto_of_tendsto'

added theorem le_of_tendsto_of_tendsto

added theorem le_on_closure

added theorem left_nhdsWithin_Ioc_neBot

added theorem left_nhdsWithin_Ioo_neBot

added theorem lt_mem_nhds

added theorem lt_subset_interior_le

added theorem map_coe_Iio_atTop

added theorem map_coe_Ioi_atBot

added theorem map_coe_Ioo_atBot

added theorem map_coe_Ioo_atTop

added theorem map_coe_atBot_of_Ioo_subset

added theorem map_coe_atTop_of_Ioo_subset

added theorem mem_nhdsWithin_Ici_iff_exists_Icc_subset

added theorem mem_nhdsWithin_Ici_iff_exists_Ico_subset'

added theorem mem_nhdsWithin_Ici_iff_exists_Ico_subset

added theorem mem_nhdsWithin_Ici_iff_exists_mem_Ioc_Ico_subset

added theorem mem_nhdsWithin_Iic_iff_exists_Icc_subset

added theorem mem_nhdsWithin_Iic_iff_exists_Ioc_subset'

added theorem mem_nhdsWithin_Iic_iff_exists_Ioc_subset

added theorem mem_nhdsWithin_Iic_iff_exists_mem_Ico_Ioc_subset

added theorem mem_nhdsWithin_Iio_iff_exists_Ico_subset

added theorem mem_nhdsWithin_Iio_iff_exists_Ioo_subset'

added theorem mem_nhdsWithin_Iio_iff_exists_Ioo_subset

added theorem mem_nhdsWithin_Iio_iff_exists_mem_Ico_Ioo_subset

added theorem mem_nhdsWithin_Ioi_iff_exists_Ioc_subset

added theorem mem_nhdsWithin_Ioi_iff_exists_Ioo_subset'

added theorem mem_nhdsWithin_Ioi_iff_exists_Ioo_subset

added theorem mem_nhdsWithin_Ioi_iff_exists_mem_Ioc_Ioo_subset

added theorem mem_nhds_iff_exists_Ioo_subset'

added theorem mem_nhds_iff_exists_Ioo_subset

added theorem nhdsWithin_Icc_eq_nhdsWithin_Ici

added theorem nhdsWithin_Icc_eq_nhdsWithin_Iic

added theorem nhdsWithin_Ici_basis'

added theorem nhdsWithin_Ici_basis

added theorem nhdsWithin_Ici_basis_Ico

added theorem nhdsWithin_Ici_eq''

added theorem nhdsWithin_Ici_eq'

added theorem nhdsWithin_Ici_neBot

added theorem nhdsWithin_Ici_self_neBot

added theorem nhdsWithin_Ico_eq_nhdsWithin_Ici

added theorem nhdsWithin_Ico_eq_nhdsWithin_Iio

added theorem nhdsWithin_Iic_basis'

added theorem nhdsWithin_Iic_basis

added theorem nhdsWithin_Iic_eq''

added theorem nhdsWithin_Iic_eq'

added theorem nhdsWithin_Iic_neBot

added theorem nhdsWithin_Iic_self_neBot

added theorem nhdsWithin_Iio_neBot

added theorem nhdsWithin_Iio_ne_bot'

added theorem nhdsWithin_Iio_self_neBot

added theorem nhdsWithin_Iio_self_ne_bot'

added theorem nhdsWithin_Ioc_eq_nhdsWithin_Iic

added theorem nhdsWithin_Ioc_eq_nhdsWithin_Ioi

added theorem nhdsWithin_Ioi_neBot'

added theorem nhdsWithin_Ioi_neBot

added theorem nhdsWithin_Ioi_self_neBot

added theorem nhdsWithin_Ioi_self_ne_bot'

added theorem nhdsWithin_Ioo_eq_nhdsWithin_Iio

added theorem nhdsWithin_Ioo_eq_nhdsWithin_Ioi

added theorem nhds_basis_Ioo'

added theorem nhds_basis_Ioo

added theorem nhds_basis_Ioo_pos

added theorem nhds_basis_Ioo_pos_of_pos

added theorem nhds_basis_abs_sub_lt

added theorem nhds_basis_zero_abs_sub_lt

added theorem nhds_bot_basis

added theorem nhds_bot_basis_Iic

added theorem nhds_bot_order

added theorem nhds_eq_infᵢ_abs_sub

added theorem nhds_eq_order

added theorem nhds_order_unbounded

added theorem nhds_top_basis

added theorem nhds_top_basis_Ici

added theorem nhds_top_order

added theorem not_tendsto_atBot_of_tendsto_nhds

added theorem not_tendsto_atTop_of_tendsto_nhds

added theorem not_tendsto_nhds_of_tendsto_atBot

added theorem not_tendsto_nhds_of_tendsto_atTop

added theorem orderTopology_of_nhds_abs

added theorem order_separated

added theorem pi_Icc_mem_nhds'

added theorem pi_Icc_mem_nhds

added theorem pi_Ici_mem_nhds'

added theorem pi_Ici_mem_nhds

added theorem pi_Ico_mem_nhds'

added theorem pi_Ico_mem_nhds

added theorem pi_Iic_mem_nhds'

added theorem pi_Iic_mem_nhds

added theorem pi_Iio_mem_nhds'

added theorem pi_Iio_mem_nhds

added theorem pi_Ioc_mem_nhds'

added theorem pi_Ioc_mem_nhds

added theorem pi_Ioi_mem_nhds'

added theorem pi_Ioi_mem_nhds

added theorem pi_Ioo_mem_nhds'

added theorem pi_Ioo_mem_nhds

added theorem preimage_neg

added theorem right_nhdsWithin_Ico_neBot

added theorem right_nhdsWithin_Ioo_neBot

added theorem supₛ_mem_closure

added theorem tendsto_Iio_atTop

added theorem tendsto_Ioi_atBot

added theorem tendsto_Ioo_atBot

added theorem tendsto_Ioo_atTop

added theorem tendsto_comp_coe_Iio_atTop

added theorem tendsto_comp_coe_Ioi_atBot

added theorem tendsto_comp_coe_Ioo_atBot

added theorem tendsto_comp_coe_Ioo_atTop

added theorem tendsto_nhds_bot_mono'

added theorem tendsto_nhds_bot_mono

added theorem tendsto_nhds_top_mono'

added theorem tendsto_nhds_top_mono

added theorem tendsto_of_tendsto_of_tendsto_of_le_of_le'

added theorem tendsto_of_tendsto_of_tendsto_of_le_of_le

added theorem tendsto_order

added theorem tendsto_order_unbounded