Image_of_Set_Difference_under_Relation

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

image-of-set-difference-under-relationproofwikirelation-theoryset-difference

Let R be a relation from S to T. Let A and B be subsets of S. Then R[A] \ R[B] ⊆ R[A \ B].

Preamble

import Mathlib.Data.Set.Basic
import Mathlib.Data.Set.Image

Formal statement

theorem Image_of_Set_Difference_under_Relation {α β : Type _} (f : α → β) (A B : Set α) : f '' A \ f '' B ⊆ f '' (A \ B) := by sorry

Source