iInf_mono' — Mathlib

English

Let α be a complete lattice and f : ι → α, g : ι' → α with the property that for every i' there exists i such that f(i) ≤ g(i'). Then iInf f ≤ iInf g.

Русский

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

LaTeX

$$$\\\\forall f : ι \\\\to α, g : ι' \\\\to α, \\\\left( \\\\forall i', \\\\exists i, f(i) \\\\le g(i') \\\\right) \\\\Rightarrow iInf f \\\\le iInf g$$$

Lean4

theorem iInf_mono' {g : ι' → α} (h : ∀ i', ∃ i, f i ≤ g i') : iInf f ≤ iInf g :=
  le_iInf fun i' => Exists.elim (h i') iInf_le_of_le

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