disjoint_image_image — Mathlib

English

If for every b in s and c in t, f(b) ≠ g(c), then the images f[S] and g[T] are disjoint.

Русский

Если для всех b ∈ s и c ∈ t выполняется f(b) ≠ g(c), то образа f[S] и g[T] неизобщаются.

LaTeX

$$$\operatorname{Disjoint}(f''s, g''t)$ under the hypothesis $\forall b\in s, \forall c\in t, f(b) \neq g(c)$$$

Lean4

theorem disjoint_image_image {f : β → α} {g : γ → α} {s : Set β} {t : Set γ} (h : ∀ b ∈ s, ∀ c ∈ t, f b ≠ g c) :
    Disjoint (f '' s) (g '' t) :=
  disjoint_iff_inf_le.mpr <| by rintro a ⟨⟨b, hb, eq⟩, c, hc, rfl⟩; exact h b hb c hc eq

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