map_iInf_of_continuousAt — Mathlib

English

If a monotone function f is continuous at the supremum of a directed family g, then f(iSup g) equals iSup of f ∘ g.

Русский

Если монотонная функция непрерывна в iSup g, то f(⨆ g) = ⨆ f ∘ g.

LaTeX

$$$Cf : ContinuousAt f (iSup g) \to Monotone f \to f(iSup g) = iSup (f \circ g)$$$

Lean4

/-- If a monotone function sending `top` to `top` is continuous at the indexed infimum over
a `Sort`, then it sends this indexed infimum to the indexed infimum of the composition. -/
theorem map_iInf_of_continuousAt {ι : Sort*} {f : α → β} {g : ι → α} (Cf : ContinuousAt f (iInf g)) (Mf : Monotone f)
    (ftop : f ⊤ = ⊤) : f (iInf g) = iInf (f ∘ g) :=
  Monotone.map_iSup_of_continuousAt (α := αᵒᵈ) (β := βᵒᵈ) Cf Mf.dual ftop

Похожие утверждения