sigmaToiUnion_bijective — Mathlib

English

Let {t_i} be a family of subsets of β such that the sets t_i are pairwise disjoint. Then the canonical map σToiUnion t from the disjoint sum Σ i, t_i to the union ⋃ i, t_i is a bijection.

Русский

Пусть {t_i} — семейство подмножеств β, члены которого попарно непересекаются. Тогда каноническое отображение σToiUnion t из разобщённой суммы Σ i, t_i на объединение ⋃ i, t_i является биекцией.

LaTeX

$$$\\operatorname{Bijective}(\\sigmaToiUnion t)$$$

Lean4

theorem sigmaToiUnion_bijective (h : Pairwise (Disjoint on t)) : Bijective (sigmaToiUnion t) :=
  ⟨sigmaToiUnion_injective t h, sigmaToiUnion_surjective t⟩

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