of_map — Mathlib

English

If the mapped lists (maps of s and t) are disjoint, then the original lists s and t are disjoint.

Русский

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

LaTeX

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

Lean4

theorem of_map {f : α → β} {s t : List α} (h : Disjoint (s.map f) (t.map f)) : Disjoint s t := fun _a has hat ↦
  h (mem_map_of_mem has) (mem_map_of_mem hat)

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