IsWF — Mathlib

English

IsWF is the definition that a type α with LT carries a WellFoundedOn relation to the set.

Русский

IsWF — это определение того, что на α с LT имеется хорошо основанное отношение к множеству.

LaTeX

$$IsWF(s) : Set α → Prop := WellFoundedOn s (\\cdot < \\cdot)$$

Lean4

/-- `s.IsWF` indicates that `<` is well-founded when restricted to `s`. -/
def IsWF (s : Set α) : Prop :=
  WellFoundedOn s (· < ·)

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