Documentation

Mathlib.Order.Restriction

Restriction of a function indexed by a preorder #

Given a preorder α and dependent function f : (i : α) → π i and a : α, one might want to consider the restriction of f to elements ≤ a. This is defined in this file as Preorder.restrictLe a f. Similarly, if we have a b : α, hab : a ≤ b and f : (i : ↑(Set.Iic b)) → π ↑i, one might want to restrict it to elements ≤ a. This is defined in this file as Preorder.restrictLe₂ hab f.

We also provide versions where the intervals are seen as finite sets, see Preorder.frestrictLe and Preorder.frestrictLe₂.

Main definitions #

def Preorder.restrictLe {α : Type u_1} [Preorder α] {π : αType u_2} (a : α) (f : (a : α) → π a) (a✝ : (Set.Iic a)) :
π a✝

Restrict domain of a function f indexed by α to elements ≤ a.

Equations
@[simp]
theorem Preorder.restrictLe_apply {α : Type u_1} [Preorder α] {π : αType u_2} (a : α) (f : (a : α) → π a) (i : (Set.Iic a)) :
restrictLe a f i = f i
def Preorder.restrictLe₂ {α : Type u_1} [Preorder α] {π : αType u_2} {a b : α} (hab : a b) (f : (a : (Set.Iic b)) → π a) (a✝ : (Set.Iic a)) :
π a✝

If a function f indexed by α is restricted to elements ≤ π, and a ≤ b, this is the restriction to elements ≤ a.

Equations
@[simp]
theorem Preorder.restrictLe₂_apply {α : Type u_1} [Preorder α] {π : αType u_2} {a b : α} (hab : a b) (f : (i : (Set.Iic b)) → π i) (i : (Set.Iic a)) :
restrictLe₂ hab f i = f i,
theorem Preorder.restrictLe₂_comp_restrictLe {α : Type u_1} [Preorder α] {π : αType u_2} {a b : α} (hab : a b) :
theorem Preorder.restrictLe₂_comp_restrictLe₂ {α : Type u_1} [Preorder α] {π : αType u_2} {a b c : α} (hab : a b) (hbc : b c) :
theorem Preorder.dependsOn_restrictLe {α : Type u_1} [Preorder α] {π : αType u_2} (a : α) :
def Preorder.frestrictLe {α : Type u_1} [Preorder α] {π : αType u_2} [LocallyFiniteOrderBot α] (a : α) (f : (i : α) → π i) (i : { x : α // x Finset.Iic a }) :
π i

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

Equations
@[simp]
theorem Preorder.frestrictLe_apply {α : Type u_1} [Preorder α] {π : αType u_2} [LocallyFiniteOrderBot α] (a : α) (f : (a : α) → π a) (i : { x : α // x Finset.Iic a }) :
frestrictLe a f i = f i
def Preorder.frestrictLe₂ {α : Type u_1} [Preorder α] {π : αType u_2} [LocallyFiniteOrderBot α] {a b : α} (hab : a b) (f : (i : { x : α // x Finset.Iic b }) → π i) (i : { x : α // x Finset.Iic a }) :
π i

If a function f indexed by α is restricted to elements ≤ b, and a ≤ b, this is the restriction to elements ≤ b. Intervals are seen as finite sets.

Equations
@[simp]
theorem Preorder.frestrictLe₂_apply {α : Type u_1} [Preorder α] {π : αType u_2} [LocallyFiniteOrderBot α] {a b : α} (hab : a b) (f : (i : { x : α // x Finset.Iic b }) → π i) (i : { x : α // x Finset.Iic a }) :
frestrictLe₂ hab f i = f i,
theorem Preorder.frestrictLe₂_comp_frestrictLe {α : Type u_1} [Preorder α] {π : αType u_2} [LocallyFiniteOrderBot α] {a b : α} (hab : a b) :
theorem Preorder.frestrictLe₂_comp_frestrictLe₂ {α : Type u_1} [Preorder α] {π : αType u_2} [LocallyFiniteOrderBot α] {a b c : α} (hab : a b) (hbc : b c) :
theorem Preorder.piCongrLeft_comp_restrictLe {α : Type u_1} [Preorder α] {π : αType u_2} [LocallyFiniteOrderBot α] {a : α} :
(Equiv.piCongrLeft (fun (i : { x : α // x Finset.Iic a }) => π i) (Equiv.IicFinsetSet a).symm) restrictLe a = frestrictLe a
theorem Preorder.piCongrLeft_comp_frestrictLe {α : Type u_1} [Preorder α] {π : αType u_2} [LocallyFiniteOrderBot α] {a : α} :
(Equiv.piCongrLeft (fun (i : (Set.Iic a)) => π i) (Equiv.IicFinsetSet a)) frestrictLe a = restrictLe a
theorem Preorder.frestrictLe_updateFinset_of_le {α : Type u_1} [Preorder α] {π : αType u_2} [LocallyFiniteOrderBot α] [DecidableEq α] {a b : α} (hab : a b) (x : (c : α) → π c) (y : (c : { x : α // x Finset.Iic b }) → π c) :
theorem Preorder.frestrictLe_updateFinset {α : Type u_1} [Preorder α] {π : αType u_2} [LocallyFiniteOrderBot α] [DecidableEq α] {a : α} (x : (a : α) → π a) (y : (b : { x : α // x Finset.Iic a }) → π b) :
@[simp]
theorem Preorder.updateFinset_frestrictLe {α : Type u_1} [Preorder α] {π : αType u_2} [LocallyFiniteOrderBot α] [DecidableEq α] (a : α) (x : (a : α) → π a) :
theorem Preorder.dependsOn_frestrictLe {α : Type u_1} [Preorder α] {π : αType u_2} [LocallyFiniteOrderBot α] (a : α) :