iInter_inv — Mathlib

English

For any family of subsets s_i ⊆ α, the inverse of their intersection equals the intersection of the inverses: (⋂ i, s_i)^{-1} = ⋂ i, (s_i)^{-1}.

Русский

Для любой семейства подмножеств s_i ⊆ α обратное по отношению к их пересечению равно пересечению обратных: (⋂ i, s_i)^{-1} = ⋂ i, s_i^{-1}.

LaTeX

$$$\\left(\\bigcap_i s_i\\right)^{-1} = \\bigcap_i (s_i)^{-1}$$$

Lean4

@[to_additive (attr := simp)]
theorem iInter_inv (s : ι → Set α) : (⋂ i, s i)⁻¹ = ⋂ i, (s i)⁻¹ :=
  preimage_iInter

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