of_image — Mathlib

English

If the images f''s and f''t are disjoint, then s and t are disjoint.

Русский

Если образы f[S] и f[T] непересекаются, то S и T непересекаются.

LaTeX

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

Lean4

theorem _root_.Disjoint.of_image (h : Disjoint (f '' s) (f '' t)) : Disjoint s t :=
  disjoint_iff_inf_le.mpr fun _ hx => disjoint_left.1 h (mem_image_of_mem _ hx.1) (mem_image_of_mem _ hx.2)

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