Theorems · Theorem · order theory

Monotone.ciSup_comp_tendsto_atTop

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

If f is a monotone function with bounded range and g tends to atTop along a nontrivial filter, then the indexed supremum of f ∘ g is equal to the indexed supremum of f. The assumption BddAbove (range f) can be omitted, if the codomain of f is a conditionally complete linear order or a complete lattice, see below.

Defined in

Mathlib.Order.Filter.AtTopBot.CompleteLattice

Cited by

4 results in Mathlib

Foundations

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

Assumes

PreorderConditionallyCompleteLatticeFilter.NeBot