Theorems · Definition · order theory

Preorder.frestrictLe

{α : Type u_1} →
  [inst : Preorder α] →
    {π : α → Type u_2} → [inst_1 : LocallyFiniteOrderBot α] → (a : α) → ((i : α) → π i) → (i : ↥(Finset.Iic a)) → π ↑i

Restrict domain of a function f indexed by α to elements ≤ a, seen as a finite set.

Defined in

Mathlib.Order.Restriction

Cited by

43 results in Mathlib

Foundations

Depth 55 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderLocallyFiniteOrderBot