Theorems · Theorem · order theory

Antitone.iSup_comp_tendsto_atBot

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

If f is an antitone function taking values in a complete lattice and g tends to atBot 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

1 results in Mathlib

Foundations

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

Assumes

PreorderConditionallyCompleteLatticeOrderTopFilter.NeBot