sUnion_inv — Mathlib

English

The inverse of the sUnion of a family of sets equals the union of inverses: (⋃₀ S)^{-1} = ⋃ s ∈ S, s^{-1}.

Русский

Обратное к объединению множества всех элементов: (⋃₀ S)^{-1} = ⋃ s ∈ S, s^{-1}.

LaTeX

$$$\\left(\\bigcup^{\\;}_{0} S\\right)^{-1} = \\bigcup_{s \\in S} s^{-1}$$$

Lean4

@[to_additive (attr := simp)]
theorem sUnion_inv (S : Set (Set α)) : (⋃₀ S)⁻¹ = ⋃ s ∈ S, s⁻¹ :=
  preimage_sUnion

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