iInter₂_mono — Mathlib

English

If s(i)(j) ⊆ t(i)(j) for all i, j, then ∩_i ∩_j s(i)(j) ⊆ ∩_i ∩_j t(i)(j).

Русский

Если s(i)(j) ⊆ t(i)(j) для всех i, j, тогда ∩_i ∩_j s(i)(j) ⊆ ∩_i ∩_j t(i)(j).

LaTeX

$$$\forall i,\forall j,\ s_{ij} \subseteq t_{ij} \Rightarrow \bigcap_{i} \bigcap_{j} s_{ij} \subseteq \bigcap_{i} \bigcap_{j} t_{ij}$$$

Lean4

theorem iInter₂_mono {s t : ∀ i, κ i → Set α} (h : ∀ i j, s i j ⊆ t i j) : ⋂ (i) (j), s i j ⊆ ⋂ (i) (j), t i j :=
  iInf₂_mono h

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