disjoint_map — Mathlib

English

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

Русский

Если f инъективно отображает элементы, то образы s и t под f также расходятся.

LaTeX

$$$ \\text{Disjoint } s t \\Rightarrow \\text{Disjoint } (s.map f) (t.map f) $$$

Lean4

/-- The images of disjoint lists under an injective map are disjoint -/
theorem disjoint_map {f : α → β} {s t : List α} (hf : Function.Injective f) (h : Disjoint s t) :
    Disjoint (s.map f) (t.map f) :=
  by
  rw [← pmap_eq_map (fun _ _ ↦ trivial), ← pmap_eq_map (fun _ _ ↦ trivial)]
  exact disjoint_pmap _ _ (fun _ _ _ _ h' ↦ hf h') h

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