Theorems · Definition · order theory

Set.IciExtend

{α : Type u_1} → {β : Type u_2} → [inst : LinearOrder α] → {a : α} → (↑(Set.Ici a) → β) → α → β

Extend a function [a, ∞) → β to a map α → β.

Defined in

Mathlib.Order.Interval.Set.ProjIcc

Cited by

9 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext

Assumes

LinearOrder