English
Let s,t be Finset α and f : α → β. If f is injective, then Disjoint (s.image f) (t.image f) if and only if Disjoint s t.
Русский
Пусть s, t — конечные множества α и f: α → β инъективна. Тогда непересечение образов s и t при отображении f эквивалентно непересечению самих множеств: Disjoint (image f s) (image f t) ⇔ Disjoint s t.
LaTeX
$$$\\operatorname{Disjoint}(\\operatorname{image} f\\, s)(\\operatorname{image} f\\, t) \\iff \\operatorname{Disjoint}(s,t)$$$
Lean4
@[simp]
theorem disjoint_image {s t : Finset α} {f : α → β} (hf : Injective f) :
Disjoint (s.image f) (t.image f) ↔ Disjoint s t :=
mod_cast Set.disjoint_image_iff hf (s := s) (t := t)
