ciInf_mono — Mathlib

English

If f ≤ g pointwise and f is bounded below, then iInf f ≤ iInf g.

Русский

Если f(x) ≤ g(x) для всех x и f имеет нижнюю грань, то iInf f ≤ iInf g.

LaTeX

$$BddBelow(range f) → (∀ x, f(x) ≤ g(x)) → iInf f ≤ iInf g$$

Lean4

/-- The indexed infimum of two functions are comparable if the functions are pointwise comparable -/
@[gcongr low]
theorem ciInf_mono {f g : ι → α} (B : BddBelow (range f)) (H : ∀ x, f x ≤ g x) : iInf f ≤ iInf g :=
  ciSup_mono (α := αᵒᵈ) B H

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