Preimage_of_Set_Difference_under_Mapping
Provedpreimages-under-mappingsproofwikiset-difference
Let f: S → T be a mapping. Let T₁ and T₂ be subsets of T. Then f⁻¹[T₁ \ T₂] = f⁻¹[T₁] \ f⁻¹[T₂].
Preamble
import Mathlib.Data.Set.Function
Formal statement
theorem Preimage_of_Set_Difference_under_Mapping {α β : Type _} (f : α → β) (T₁ T₂ : Set β) : f ⁻¹' (T₁ \ T₂) = f ⁻¹' T₁ \ f ⁻¹' T₂ := by sorrySource