ciInf_comp_tendsto_atTop_of_linearOrder

English

If f is Antitone and g tends to atTop, then the indexed infimum of f ∘ g equals the infimum of f.

Русский

Если f антитонна и g стремится к atTop, инфимум по f ∘ g равен инфимума f.

LaTeX

$$$$\text{Antitone}(f) \rightarrow (\operatorname{Tendsto} g\ l\ atTop) \Rightarrow \operatorname{iInf}(a \mapsto f(g(a))) = \operatorname{iInf}(b \mapsto f(b))$$$$

Lean4

/-- If `f` is an antitone function taking values in a conditionally complete linear order
and `g` tends to `atTop` along a nontrivial filter,
then the indexed infimum of `f ∘ g` is equal to the indexed infimum of `f`. -/
theorem _root_.Antitone.ciInf_comp_tendsto_atTop_of_linearOrder [Preorder β] [ConditionallyCompleteLinearOrder γ]
    {l : Filter α} [l.NeBot] {f : β → γ} (hf : Antitone f) {g : α → β} (hg : Tendsto g l atTop) :
    ⨅ a, f (g a) = ⨅ b, f b :=
  hf.dual_left.ciInf_comp_tendsto_atBot_of_linearOrder hg

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