Theorems · Theorem · general topology

Monotone.lowerBounds_range_comp_tendsto_atBot

∀ {α : 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.atBot → lowerBounds (Set.range (f ∘ g)) = lowerBounds (Set.range f)

If f is a monotone function and g tends to atBot along a nontrivial filter. then the lower bounds of the range of f ∘ g are the same as the lower bounds of the range of f.

Defined in

Mathlib.Order.Filter.AtTopBot.Tendsto

Cited by

1 results in Mathlib

Foundations

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

Assumes

PreorderPreorderFilter.NeBot