biInf_mono — Mathlib

English

Let p,q : ι → Prop with p i → q i. Then ⨅ (i) (_ : q i), f i ≤ ⨅ (i) (_ : p i), f i.

Русский

Пусть p,q : ι → Prop и p i → q i. Тогда ⨅_{i: q i} f i ≤ ⨅_{i: p i} f i.

LaTeX

$$$\\\\forall i, p i \\\\Rightarrow q i \\\\Rightarrow \\\\bigwedge_{i: q i} f(i) \\\\le \\\\bigwedge_{i: p i} f(i)$$$

Lean4

theorem biInf_mono {p q : ι → Prop} (hpq : ∀ i, p i → q i) : ⨅ (i) (_ : q i), f i ≤ ⨅ (i) (_ : p i), f i :=
  iInf_mono fun i => iInf_const_mono (hpq i)

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