Disjoint — Mathlib

English

A scheme is disjoint if the children of every node are pairwise disjoint.

Русский

Схема диссоциирована, если у узла все дети попарно непересекаются.

LaTeX

$$$ \forall l: List\beta, \; \text{Pairwise }(a,b) \mapsto \mathrm{Disjoint}(A(a::l), A(b::l)). $$$

Lean4

/-- A scheme is disjoint if the children of each set of pairwise disjoint. -/
protected def Disjoint : Prop :=
  ∀ l : List β, Pairwise fun a b => Disjoint (A (a :: l)) (A (b :: l))

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