preimage_val_sUnion — Mathlib

English

The preimage of a union under Subtype.val distributes: A ∩ (⋃ S) equals ⋃ { A ∩ B | B ∈ S }.

Русский

Предобраз объединения по Subtype.val распределяется: A ∩ (⋃ S) = ⋃{ A ∩ B | B ∈ S }.

LaTeX

$$$A \\cap \\bigcup S = \\bigcup_{B \\in S} (A \\cap B)$$$

Lean4

theorem preimage_val_sUnion : A ↓∩ (⋃₀ S) = ⋃₀ {(A ↓∩ B) | B ∈ S} :=
  by
  rw [← Set.image, sUnion_image]
  simp_rw [sUnion_eq_biUnion, preimage_iUnion]

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