of_image_finset — Mathlib

English

Let s,t be Finset α and f: α → β. Then if s.image f and t.image f are disjoint, then s and t are disjoint.

Русский

Пусть s,t — Finset α и f: α → β. Тогда если образа s и t под f не пересекаются, то сами множества s и t не пересекаются.

LaTeX

$$$ \\operatorname{Disjoint}(\\operatorname{image} f\, s)(\\operatorname{image} f\, t) \\Rightarrow \\operatorname{Disjoint} s t $$$

Lean4

theorem _root_.Disjoint.of_image_finset {s t : Finset α} {f : α → β} (h : Disjoint (s.image f) (t.image f)) :
    Disjoint s t :=
  disjoint_iff_ne.2 fun _ ha _ hb =>
    ne_of_apply_ne f <| h.forall_ne_finset (mem_image_of_mem _ ha) (mem_image_of_mem _ hb)

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