coprodᵢ_mono — Mathlib

English

If hf i is a monotone relation between f₁ i and f₂ i for all i, then Coprodᵢ f₁ ≤ Coprodᵢ f₂.

Русский

Если hf i задаёт монотонность между f₁ i и f₂ i для всех i, то Coprodᵢ f₁ ≤ Coprodᵢ f₂.

LaTeX

$$coprodᵢ_mono (hf : ∀ i, f₁ i ≤ f₂ i) : Filter.coprodᵢ f₁ ≤ Filter.coprodᵢ f₂$$

Lean4

@[mono]
theorem coprodᵢ_mono (hf : ∀ i, f₁ i ≤ f₂ i) : Filter.coprodᵢ f₁ ≤ Filter.coprodᵢ f₂ :=
  iSup_mono fun i => comap_mono (hf i)

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