disjoint_range_iff — Mathlib

English

Let x: β → α and y: γ → α. The ranges are disjoint if and only if x i ≠ y j for all i, j.

Русский

Пусть x: β → α и y: γ → α. Образы значений функций x и y по росту не пересекаются тогда и только тогда, когда для всех i и j пары x(i) и y(j) не равны.

LaTeX

$$$Disjoint(\operatorname{range} x, \operatorname{range} y) \iff \forall i:\beta, \forall j:\gamma, x(i) \neq y(j)$$$

Lean4

theorem disjoint_range_iff {β γ : Sort*} {x : β → α} {y : γ → α} : Disjoint (range x) (range y) ↔ ∀ i j, x i ≠ y j := by
  simp [Set.disjoint_iff_forall_ne]

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