Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-16 07:32 f40cd88c

View on Github →

chore(topology/algebra/ordered): move some lemmas to a new file (#9745)

Estimated changes

deleted theorem infi_eq_of_tendsto
deleted theorem is_glb_of_tendsto
deleted theorem is_lub_of_tendsto
deleted theorem monotone.ge_of_tendsto
deleted theorem monotone.le_of_tendsto
deleted theorem supr_eq_of_tendsto
deleted theorem tendsto_at_bot_cinfi
deleted theorem tendsto_at_bot_csupr
deleted theorem tendsto_at_bot_infi
deleted theorem tendsto_at_bot_is_glb
deleted theorem tendsto_at_bot_is_lub
deleted theorem tendsto_at_bot_supr
deleted theorem tendsto_at_top_cinfi
deleted theorem tendsto_at_top_csupr
deleted theorem tendsto_at_top_infi
deleted theorem tendsto_at_top_is_glb
deleted theorem tendsto_at_top_is_lub
deleted theorem tendsto_at_top_supr
deleted theorem tendsto_of_monotone
added theorem infi_eq_of_tendsto
added theorem is_glb_of_tendsto
added theorem is_lub_of_tendsto
added theorem monotone.ge_of_tendsto
added theorem monotone.le_of_tendsto
added theorem supr_eq_of_tendsto
added theorem tendsto_at_bot_cinfi
added theorem tendsto_at_bot_csupr
added theorem tendsto_at_bot_infi
added theorem tendsto_at_bot_is_glb
added theorem tendsto_at_bot_is_lub
added theorem tendsto_at_bot_supr
added theorem tendsto_at_top_cinfi
added theorem tendsto_at_top_csupr
added theorem tendsto_at_top_infi
added theorem tendsto_at_top_is_glb
added theorem tendsto_at_top_is_lub
added theorem tendsto_at_top_supr
added theorem tendsto_of_monotone