disjoint_map — Mathlib

English

Disjointness is preserved under mapping by an embedding: Disjoint (s.map f) (t.map f) ↔ Disjoint s t.

Русский

Не пересекаются множества сохраняется после отображения через вложение.

LaTeX

$$$\mathrm{Disjoint}(\mathrm{Finset.map}\ f\ s, \mathrm{Finset.map}\ f\ t) \iff \mathrm{Disjoint}(s,t)$$$

Lean4

@[simp]
theorem disjoint_map {s t : Finset α} (f : α ↪ β) : Disjoint (s.map f) (t.map f) ↔ Disjoint s t :=
  mod_cast Set.disjoint_image_iff f.injective (s := s) (t := t)

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