ext
α : Type u_1
β : Type u_2
ι : Type u_3
s : ι → Set α
h : univ.PairwiseDisjoint s
⊢ Set.range ⇑h.sigmaSubtypeEmbedding = ⋃ i, s i
case h
α : Type u_1
β : Type u_2
ι : Type u_3
s : ι → Set α
h : univ.PairwiseDisjoint s
x✝ : α
⊢ x✝ ∈ Set.range ⇑h.sigmaSubtypeEmbedding ↔ x✝ ∈ ⋃ i, s i