Theorems · Theorem · order theory

Antitone.ciSup_comp_tendsto_atBot

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

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

2 results in Mathlib

Foundations

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

Assumes

PreorderConditionallyCompleteLatticeFilter.NeBot