Theorems · Inductive type · order theory

ChainCompletePartialOrder.IsAdmissible

{α : Type u_1} → [ChainCompletePartialOrder α] → α → (α → α) → Set α → Prop

An admissible set for given x : α and f : α → α has x, the base point, as a least element and is closed under applying f and cSup.

Defined in

Mathlib.Order.BourbakiWitt

Cited by

8 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

ChainCompletePartialOrder