sInter_inv — Mathlib

English

For a collection S of subsets of α, the inverse of the intersection S.sInter equals the intersection over S of the inverses: (S.sInter)^{-1} = ⋂ s ∈ S, s^{-1}.

Русский

Для коллекции S подмножеств α обратное пересечения S.sInter равно пересечению по всем s∈S от s^{-1}.

LaTeX

$$$S.sInter^{-1} = \\bigcap_{s \\in S} s^{-1}$$$

Lean4

@[to_additive (attr := simp)]
theorem sInter_inv (S : Set (Set α)) : (⋂₀ S)⁻¹ = ⋂ s ∈ S, s⁻¹ :=
  preimage_sInter

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