Commit 2021-08-03 16:52 c543ec9a

View on Github →

feat(topology/algebra/ordered/basic): sequences tending to Inf/Sup (#8524) We show that there exist monotone sequences tending to the Inf/Sup of a set in a conditionally complete linear order, as well as several related lemmas expressed in terms of is_lub and is_glb.

Estimated changes

Modified src/topology/algebra/ordered/basic.lean

added theorem exists_seq_strict_antimono_tendsto

added theorem exists_seq_strict_mono_tendsto

added theorem exists_seq_tendsto_Inf

added theorem exists_seq_tendsto_Sup

added theorem is_glb.exists_seq_monotone_tendsto'

added theorem is_glb.exists_seq_monotone_tendsto

added theorem is_glb.exists_seq_strict_mono_tendsto_of_not_mem'

added theorem is_glb.exists_seq_strict_mono_tendsto_of_not_mem

added theorem is_glb_of_mem_closure

added theorem is_lub.exists_seq_monotone_tendsto'

added theorem is_lub.exists_seq_monotone_tendsto

added theorem is_lub.exists_seq_strict_mono_tendsto_of_not_mem'

added theorem is_lub.exists_seq_strict_mono_tendsto_of_not_mem

added theorem is_lub_of_mem_closure