image_diff — Mathlib

English

If f is injective on s, then f''(s \\ t) = f''s \\ f''(s ∩ t).

Русский

Если f инъективна на s, то образ разности s \\ t равен образу s минус образ s ∩ t: f''(s \\ t) = f''s \\ f''(s ∩ t).

LaTeX

$$$\\forall t\\subseteq α\\, (h:\\, s\\ InjOn\\ f) \\Rightarrow f''(s\\setminus t) = f''s \\setminus f''(s\\cap t).$$$

Lean4

theorem image_diff {t : Set α} (h : s.InjOn f) : f '' (s \ t) = f '' s \ f '' (s ∩ t) :=
  by
  refine
    subset_antisymm (subset_diff.2 ⟨image_mono diff_subset, ?_⟩)
      (diff_subset_iff.2 (by rw [← image_union, inter_union_diff]))
  exact Disjoint.image disjoint_sdiff_inter h diff_subset inter_subset_left

Похожие утверждения