sUnion_div — Mathlib

English

The division by a set of sets distributes over the union: (⋃₀ S) / t = ⋃ s ∈ S, s / t.

Русский

Деление объединения множества множеств по t равно объединению частных каждого множества по t: (⋃₀ S) / t = ⋃_{s ∈ S} (s / t).

LaTeX

$$$$ (\bigcup_0 S) / t = \bigcup_{s \in S} (s / t) $$$$

Lean4

@[to_additive]
theorem sUnion_div (S : Set (Set α)) (t : Set α) : ⋃₀ S / t = ⋃ s ∈ S, s / t :=
  image2_sUnion_left ..

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