preimage_iUnion₂ — Mathlib

English

For any function f, family s_{i,j}, we have f^{-1}(⋃ i (⋃ j, s_{i j})) = ⋃ i (⋃ j, f^{-1}(s_{i j})).

Русский

Для любой функции f, семейства s_{i j} выполняется f^{-1}(⋃_{i} ⋃_{j} s_{i j}) = ⋃_{i} ⋃_{j} f^{-1}(s_{i j}).

LaTeX

$$$f^{-1}\Bigl(\bigcup_i \bigcup_j s_{i j}\Bigr) = \bigcup_i \bigcup_j f^{-1}(s_{i j})$$$

Lean4

theorem preimage_iUnion₂ {f : α → β} {s : ∀ i, κ i → Set β} : (f ⁻¹' ⋃ (i) (j), s i j) = ⋃ (i) (j), f ⁻¹' s i j := by
  simp_rw [preimage_iUnion]

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