disjoint_image_iff — Mathlib

English

For any injective f, the images f[S] and f[T] are disjoint iff S and T are disjoint.

Русский

Для инъективной f образа f[S] и f[T] непересекаются тогда и только тогда, когда S и T непересекаются.

LaTeX

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

Lean4

@[simp]
theorem disjoint_image_iff (hf : Injective f) : Disjoint (f '' s) (f '' t) ↔ Disjoint s t :=
  ⟨Disjoint.of_image, disjoint_image_of_injective hf⟩

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