iUnion₂_mono' — Mathlib

English

If for all i there exists i', j' with s(i)(j) ⊆ t(i')(j'), then ⋃_i ⋃_j s(i)(j) ⊆ ⋃_{i'} ⋃_{j'} t(i')(j').

Русский

Если для всех (i,j) найдётся (i',j') с s(i)(j) ⊆ t(i')(j'), тогда ⋃_i ⋃_j s(i)(j) ⊆ ⋃_{i'} ⋃_{j'} t(i')(j').

LaTeX

$$$\forall i,\forall j,\ Exists \! i', j',\ s_{ij} \subseteq t_{i' j'} \Rightarrow \bigcup_{i} \bigcup_{j} s_{ij} \subseteq \bigcup_{i'} \bigcup_{j'} t_{i' j'}$$$

Lean4

theorem iUnion₂_mono' {s : ∀ i, κ i → Set α} {t : ∀ i', κ' i' → Set α} (h : ∀ i j, ∃ i' j', s i j ⊆ t i' j') :
    ⋃ (i) (j), s i j ⊆ ⋃ (i') (j'), t i' j' :=
  iSup₂_mono' h

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