sumSet_range — Mathlib

English

For disjoint subsets s and t of α, the range of the embedding sumSet h is exactly s ∪ t.

Русский

Для попарно непересекающихся подмножеств s и t множества α диапазон отображения sumSet h равен s ∪ t.

LaTeX

$$$\operatorname{range}(\mathrm{sumSet}(h)) = s \cup t$$$

Lean4

@[simp]
theorem sumSet_range {s t : Set α} (h : Disjoint s t) : range (Function.Embedding.sumSet h) = s ∪ t := by
  simp [Set.ext_iff]

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