biSup_mono — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem biSup_mono {p q : ι → Prop} (hpq : ∀ i, p i → q i) : ⨆ (i) (_ : p i), f i ≤ ⨆ (i) (_ : q i), f i :=
  iSup_mono fun i => iSup_const_mono (hpq i)

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