div_sUnion — Mathlib

English

A fixed set s divided by the union of a family T of sets equals the union over t in T of the divisions s / t: s / ⋃₀ T = ⋃_{t ∈ T} (s / t).

Русский

Фиксированное множество s делится на объединение семей T множества: s / ⋃₀ T = ⋃_{t∈T} (s / t).

LaTeX

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

Lean4

@[to_additive]
theorem div_sUnion (s : Set α) (T : Set (Set α)) : s / ⋃₀ T = ⋃ t ∈ T, s / t :=
  image2_sUnion_right ..

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