iUnion₂_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 \bigcup_{i} \bigcup_{j} s_{ij} \subseteq \bigcup_{i} \bigcup_{j} t_{ij}$$$

Lean4

theorem iUnion₂_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 :=
  iSup₂_mono h

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