Theorems · Theorem · general topology

Antitone.upperBounds_range_comp_tendsto_atBot

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

If f is an antitone function and g tends to atBot 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.

Defined in

Mathlib.Order.Filter.AtTopBot.Tendsto

Cited by

0 results in Mathlib

Foundations

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

Assumes

PreorderPreorderFilter.NeBot