Theorems · Theorem · order theory

Monotone.iSup_comp_tendsto_atTop

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

If f is a monotone function taking values in a complete lattice and g tends to atTop along a nontrivial filter, then the indexed supremum of f ∘ g is equal to the indexed supremum of f.

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

PreorderConditionallyCompleteLatticeOrderTopFilter.NeBot