sigmaSet_preimage — Mathlib

English

For a pairwise disjoint family h : Pairwise (Disjoint on s) and any index i and set r, the preimage under Sigma.mk(i) of sigmaSet(h)^{-1}(r) is r ∩ s_i.

Русский

Для пары несовпадающих семей h и любого индекса i и множества r верно: preimage(Sigma.mk(i)) от sigmaSet(h)^{-1}(r) равен r ∩ s_i.

LaTeX

$$$\Sigma\!\text{mk}(i)^{-1}\big(\big(\mathrm{sigmaSet}(h)\big)^{-1}(r)\big) = r \cap s_i$$$

Lean4

@[simp]
theorem sigmaSet_preimage {s : ι → Set α} (h : Pairwise (Disjoint on s)) (i : ι) (r : Set α) :
    Sigma.mk i ⁻¹' (Function.Embedding.sigmaSet h ⁻¹' r) = r ∩ s i := by simp [Set.ext_iff]

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