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

• Preorder.restrictLe a f: Restricts the function f to the variables indexed by elements ≤ a.

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

• Preorder.restrictLe a = (Set.Iic a).restrict

@[simp]

theorem Preorder.restrictLe_apply {α : Type u_1} [Preorder α] {π : α → Type u_2} (a : α) (f : (a : α) → π a) (i : ↑(Set.Iic a)) : Preorder.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

• Preorder.restrictLe₂ hab = Set.restrict₂ ⋯

@[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)) : Preorder.restrictLe₂ hab f i = f ⟨↑i, ⋯⟩

theorem Preorder.restrictLe₂_comp_restrictLe {α : Type u_1} [Preorder α] {π : α → Type u_2} {a b : α} (hab : a ≤ b) : Preorder.restrictLe₂ hab ∘ Preorder.restrictLe b = Preorder.restrictLe a

theorem Preorder.restrictLe₂_comp_restrictLe₂ {α : Type u_1} [Preorder α] {π : α → Type u_2} {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) : Preorder.restrictLe₂ hab ∘ Preorder.restrictLe₂ hbc = Preorder.restrictLe₂ ⋯

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 ≤ α, seen as a finite set.

Equations

• Preorder.frestrictLe a = (Finset.Iic a).restrict

@[simp]

theorem Preorder.frestrictLe_apply {α : Type u_1} [Preorder α] {π : α → Type u_2} [LocallyFiniteOrderBot α] (a : α) (f : (a : α) → π a) (i : { x : α // x ∈ Finset.Iic a }) : Preorder.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

• Preorder.frestrictLe₂ hab = Finset.restrict₂ ⋯

@[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 }) : Preorder.frestrictLe₂ hab f i = f ⟨↑i, ⋯⟩

theorem Preorder.frestrictLe₂_comp_frestrictLe {α : Type u_1} [Preorder α] {π : α → Type u_2} [LocallyFiniteOrderBot α] {a b : α} (hab : a ≤ b) : Preorder.frestrictLe₂ hab ∘ Preorder.frestrictLe b = Preorder.frestrictLe a

theorem Preorder.frestrictLe₂_comp_frestrictLe₂ {α : Type u_1} [Preorder α] {π : α → Type u_2} [LocallyFiniteOrderBot α] {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) : Preorder.frestrictLe₂ hab ∘ Preorder.frestrictLe₂ hbc = Preorder.frestrictLe₂ ⋯