English
Let s and t be disjoint subsets of α, and let u be a subset of α with s ⊆ u and t ⊆ u. If f is injective on u, then the images f''s and f''t are disjoint: f''s ∩ f''t = ∅.
Русский
Пусть s, t ⊆ α не пересекаются, и пусть u ⊆ α содержит обе: s ⊆ u и t ⊆ u. Если f инъективна на u, то образы f''s и f''t не пересекаются: f''s ∩ f''t = ∅.
LaTeX
$$$\\forall s,t,u \\subseteq \\alpha\\,\\forall f:\\\\alpha \\to \\beta,\\\\ Disjoint(s,t) \\\\land u.InjOn f \\\\land s \\subseteq u \\\\land t \\subseteq u \\\\Rightarrow Disjoint(f''s)(f''t).$$$
Lean4
theorem _root_.Disjoint.image {s t u : Set α} {f : α → β} (h : Disjoint s t) (hf : u.InjOn f) (hs : s ⊆ u)
(ht : t ⊆ u) : Disjoint (f '' s) (f '' t) :=
by
rw [disjoint_iff_inter_eq_empty] at h ⊢
rw [← hf.image_inter hs ht, h, image_empty]
