Theorems · Theorem · order theory

Pi.monotoneUncurry_coe

∀ (α : Type u_1) (β : α → Type u_2) (γ : (a : α) → β a → Type u_3) [inst : (x : α) → (y : β x) → Preorder (γ x y)]
  (f : (x : α) → (y : β x) → γ x y) (x : Sigma β), (Pi.monotoneUncurry α β γ) f x = Sigma.uncurry f x

Defined in

Mathlib.Control.LawfulFix

Cited by

0 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms

Assumes

Preorder