Theorems · Theorem · general topology

Monotone.upperBounds_range_comp_tendsto_atTop

∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : Preorder γ] {l : Filter α} [l.NeBot]
  {f : β → γ},
  Monotone f →
    ∀ {g : α → β}, Filter.Tendsto g l Filter.atTop → upperBounds (Set.range (f ∘ g)) = upperBounds (Set.range f)

If f is a monotone function and g tends to atTop along a nontrivial filter. then the upper bounds of the range of f ∘ g are the same as the upper bounds of the range of f. This lemma together with exists_seq_monotone_tendsto_atTop_atTop below is useful to reduce a statement about a monotone family indexed by a type with countably generated atTop (e.g., ℝ) to the case of a family indexed by natural numbers.

Defined in

Mathlib.Order.Filter.AtTopBot.Tendsto

Cited by

3 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderPreorderFilter.NeBot