disjoint_map_map — Mathlib

English

Let f: α→γ and g: β→γ. Then Disjoint (s.map f) (t.map g) iff ∀ a ∈ s, ∀ b ∈ t, f a ≠ g b.

Русский

Пусть f: α→γ и g: β→γ. Тогда Disjoint (s.map f) (t.map g) эквивалентно ∀ a ∈ s, ∀ b ∈ t, f a ≠ g b.

LaTeX

$$$Disjoint (s.map f) (t.map g) \\iff \\forall a \\in s, \\forall b \\in t, f a \\neq g b$$$

Lean4

theorem disjoint_map_map {f : α → γ} {g : β → γ} {s : Multiset α} {t : Multiset β} :
    Disjoint (s.map f) (t.map g) ↔ ∀ a ∈ s, ∀ b ∈ t, f a ≠ g b := by simp [disjoint_iff_ne]

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