disjoint_image_of_injective — Mathlib

English

If f is injective and s,t are disjoint, then their images under f are disjoint.

Русский

Если f инъективна и s ∩ t = ∅, то f[S] ∩ f[T] = ∅.

LaTeX

$$$\operatorname{Disjoint}(f''s, f''t)$ given $\operatorname{Injective}(f)$ and $\operatorname{Disjoint}(s,t)$$$

Lean4

theorem disjoint_image_of_injective (hf : Injective f) {s t : Set α} (hd : Disjoint s t) : Disjoint (f '' s) (f '' t) :=
  disjoint_image_image fun _ hx _ hy => hf.ne fun H => Set.disjoint_iff.1 hd ⟨hx, H.symm ▸ hy⟩

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