ext
α : Type u_1
β : Type u_2
ι : Type u_3
s t : Set α
h : Disjoint s t
⊢ range ⇑h.sumSubtypeEmbedding = s ∪ t
case h
α : Type u_1
β : Type u_2
ι : Type u_3
s t : Set α
h : Disjoint s t
x✝ : α
⊢ x✝ ∈ range ⇑h.sumSubtypeEmbedding ↔ x✝ ∈ s ∪ t