Antitone — Mathlib

English

A scheme A is antitone if every child is contained in its parent: for all l and a, A(a :: l) ⊆ A(l).

Русский

Схема A антимонотонна: каждый ребенок содержится в родителе, т.е. A(a::l) ⊆ A(l).

LaTeX

$$$ \forall l: List\beta, \forall a: \beta, A(a::l) \subseteq A(l). $$$

Lean4

/-- A scheme is antitone if each set contains its children. -/
protected def Antitone : Prop :=
  ∀ l : List β, ∀ a : β, A (a :: l) ⊆ A l

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