iUnion_iInter_subset — Mathlib

English

For a double-indexed family s(i,j), the union over j of the intersection over i is a subset of the intersection over i of the union over j: (⋃_j ⋂_i s(i,j)) ⊆ ⋂_i ⋃_j s(i,j).

Русский

Для двухпорядкового семейства s(i,j) выполняется: ⋃_j ⋂_i s(i,j) ⊆ ⋂_i ⋃_j s(i,j).

LaTeX

$$$ \bigcup_j \bigcap_i s(i,j) \subseteq \bigcap_i \bigcup_j s(i,j) $$$

Lean4

/-- An equality version of this lemma is `iUnion_iInter_of_monotone` in `Data.Set.Finite`. -/
theorem iUnion_iInter_subset {s : ι → ι' → Set α} : (⋃ j, ⋂ i, s i j) ⊆ ⋂ i, ⋃ j, s i j :=
  iSup_iInf_le_iInf_iSup (flip s)

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