English
Let α be a type. For β, γ and x: β → α, y: γ → α, Disjoint(range x, range y) iff ∀ i ∈ β, ∀ j ∈ γ, x(i) ≠ y(j).
Русский
Пусть α — множество. Для функций 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
/-- Given a choice function `sel`, enumerates the elements of a set in the order
`a 0 = sel s`, `a 1 = sel (s \ {a 0})`, `a 2 = sel (s \ {a 0, a 1})`, ... and stops when
`sel (s \ {a 0, ..., a n}) = none`. Note that we don't require `sel` to be a choice function. -/
def enumerate : Set α → ℕ → Option α
| s, 0 => sel s
| s, n + 1 => do
let a ← sel s
enumerate (s \ { a }) n
