theorem PiBase.Formal.image_transEquiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (g : β ≃ γ) (s : Set α) : ↑(e.transEquiv g) '' s = ⇑g '' ↑e '' s

Images under a partial equivalence postcomposed with an equivalence.

theorem PiBase.WellDefined.cWComplexSpace : WellDefined CWComplexSpace