iInf_mono — Mathlib

English

Let α be a complete lattice and f,g : ι → α. If f(i) ≤ g(i) for every i, then iInf f ≤ iInf g.

Русский

Пусть α — полная решетка и f,g : ι → α. Если для каждого i выполняется f(i) ≤ g(i), то iInf f ≤ iInf g.

LaTeX

$$$\\\\forall ι, α \\\\[CompleteLattice α\\\\] (f,g : ι \\\\to α), \\\\left( \\\\forall i, f(i) \\\\le g(i) \\\\right) \\\\Rightarrow iInf f \\\\le iInf g$$$

Lean4

@[gcongr]
theorem iInf_mono (h : ∀ i, f i ≤ g i) : iInf f ≤ iInf g :=
  le_iInf fun i => iInf_le_of_le i <| h i

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