Theorems · Inductive type · order theory

PrincipalSeg

{α : Type u_4} → {β : Type u_5} → (α → α → Prop) → (β → β → Prop) → Type (max u_4 u_5)

If r is a relation on α and s in a relation on β, then f : r ≺i s is an initial segment embedding whose range is Set.Iio x for some element x. If β is a well order, this is equivalent to the embedding not being surjective.

Defined in

Mathlib.Order.InitialSeg

Cited by

73 results in Mathlib

Foundations

Depth 0 from the axioms · uses no axioms