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.

@[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.

@[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) : restrictLe₂ hab ∘ restrictLe b = restrictLe a

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

theorem Preorder.dependsOn_restrictLe {α : Type u_1} [Preorder α] {π : α → Type u_2} (a : α) : DependsOn (restrictLe a) (Set.Iic 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.

@[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.

@[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) : frestrictLe₂ hab ∘ frestrictLe b = frestrictLe a

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

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) : frestrictLe a (Function.updateFinset x (Finset.Iic b) y) = frestrictLe₂ hab y

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) : frestrictLe a (Function.updateFinset x (Finset.Iic a) y) = y

@[simp]

theorem Preorder.updateFinset_frestrictLe {α : Type u_1} [Preorder α] {π : α → Type u_2} [LocallyFiniteOrderBot α] [DecidableEq α] (a : α) (x : (a : α) → π a) : Function.updateFinset x (Finset.Iic a) (frestrictLe a x) = x

theorem Preorder.dependsOn_frestrictLe {α : Type u_1} [Preorder α] {π : α → Type u_2} [LocallyFiniteOrderBot α] (a : α) : DependsOn (frestrictLe a) (Set.Iic a)