iInf₂_mono — Mathlib

English

Let α be a complete lattice and f,g : ∀ i, κ i → α. If f i j ≤ g i j for all i and j, then ⨅ i (⨅ j, f i j) ≤ ⨅ i (⨅ j, g i j).

Русский

Пусть α — полная решетка и f,g : ∀ i, κ i → α. Если f(i,j) ≤ g(i,j) для всех i, j, то ⨅_i ⨅_j f(i,j) ≤ ⨅_i ⨅_j g(i,j).

LaTeX

$$$\\\\forall i, j, f(i,j) \\\\le g(i,j) \\\\Rightarrow \\\\bigwedge_{i} \\\\bigwedge_{j} f(i,j) \\\\le \\\\bigwedge_{i} \\\\bigwedge_{j} g(i,j)$$$

Lean4

theorem iInf₂_mono {f g : ∀ i, κ i → α} (h : ∀ i j, f i j ≤ g i j) : ⨅ (i) (j), f i j ≤ ⨅ (i) (j), g i j :=
  iInf_mono fun i => iInf_mono <| h i

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