This module contains some basic definitions and results from domain theory, intended to be used as the underlying construction of the partial_fixpoint feature. It is not meant to be used as a general purpose library for domain theory, but can be of interest to users who want to extend the partial_fixpoint machinery (e.g. mark more functions as monotone or register more monads).

This follows the corresponding Isabelle development, as also described in Alexander Krauss: Recursive Definitions of Monadic Functions.

class Lean.Order.PartialOrder (α : Sort u) : Sort (max 1 u)

A partial order is a reflexive, transitive and antisymmetric relation.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

• rel : α → α → Prop

  A “less-or-equal-to” or “approximates” relation.

  This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

• rel_refl {x : α} : rel x x

  The “less-or-equal-to” or “approximates” relation is reflexive.

• rel_trans {x y z : α} : rel x y → rel y z → rel x z

  The “less-or-equal-to” or “approximates” relation is transitive.

• rel_antisymm {x y : α} : rel x y → rel y x → x = y

  The “less-or-equal-to” or “approximates” relation is antisymmetric.

def Lean.Order.«term_⊑_» : TrailingParserDescr

A “less-or-equal-to” or “approximates” relation.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

Equations

• Lean.Order.«term_⊑_» = Lean.ParserDescr.trailingNode `Lean.Order.«term_⊑_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊑ ") (Lean.ParserDescr.cat `term 51))

theorem Lean.Order.PartialOrder.rel_of_eq {α : Sort u} [PartialOrder α] {x y : α} (h : x = y) : rel x y

def Lean.Order.chain {α : Sort u} [PartialOrder α] (c : α → Prop) : Prop

A chain is a totally ordered set (representing a set as a predicate).

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

Equations

• Lean.Order.chain c = ∀ (x y : α), c x → c y → Lean.Order.PartialOrder.rel x y ∨ Lean.Order.PartialOrder.rel y x

def Lean.Order.is_sup {α : Sort u} [PartialOrder α] (c : α → Prop) (s : α) : Prop

Equations

• Lean.Order.is_sup c s = ∀ (x : α), Lean.Order.PartialOrder.rel s x ↔ ∀ (y : α), c y → Lean.Order.PartialOrder.rel y x

theorem Lean.Order.is_sup_unique {α : Sort u_1} [PartialOrder α] {c : α → Prop} {s₁ s₂ : α} (h₁ : is_sup c s₁) (h₂ : is_sup c s₂) : s₁ = s₂

def Lean.Order.is_meet {α : Sort u} [PartialOrder α] (x y w : α) : Prop

is_meet x y w states that w is a greatest lower bound of x and y.

This is intended to be used in the construction of the strong induction principles of inductive_fixpoint and coinductive_fixpoint, and not meant to be used otherwise.

Equations

• One or more equations did not get rendered due to their size.

class Lean.Order.CCPO (α : Sort u) extends Lean.Order.PartialOrder α : Sort (max 1 u)

A chain-complete partial order (CCPO) is a partial order where every chain has a least upper bound.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

• rel : α → α → Prop
• rel_refl {x : α} : rel x x
• rel_trans {x y z : α} : rel x y → rel y z → rel x z
• rel_antisymm {x y : α} : rel x y → rel y x → x = y
• has_csup {c : α → Prop} (hc : chain c) : Exists (is_sup c)

  The least upper bound of chains exists.

noncomputable def Lean.Order.CCPO.csup {α : Sort u} [CCPO α] {c : α → Prop} (hc : chain c) : α

Equations

• Lean.Order.CCPO.csup hc = Classical.choose ⋯

theorem Lean.Order.CCPO.csup_spec {α : Sort u} [CCPO α] {c : α → Prop} (hc : chain c) : is_sup c (csup hc)

theorem Lean.Order.csup_le {α : Sort u} [CCPO α] {x : α} {c : α → Prop} (hc : chain c) : (∀ (y : α), c y → PartialOrder.rel y x) → PartialOrder.rel (CCPO.csup hc) x

theorem Lean.Order.le_csup {α : Sort u} [CCPO α] {c : α → Prop} (hc : chain c) {y : α} (hy : c y) : PartialOrder.rel y (CCPO.csup hc)

def Lean.Order.empty_chain (α : Sort u_1) : α → Prop

Equations

• Lean.Order.empty_chain α x✝ = False

theorem Lean.Order.chain_empty (α : Sort u) [PartialOrder α] : chain (empty_chain α)

noncomputable def Lean.Order.bot {α : Sort u} [CCPO α] : α

The bottom element is the least upper bound of the empty chain.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

Equations

• Lean.Order.bot = Lean.Order.CCPO.csup ⋯

def Lean.Order.«term⊥» : ParserDescr

Equations

• Lean.Order.«term⊥» = Lean.ParserDescr.node `Lean.Order.«term⊥» 1024 (Lean.ParserDescr.symbol "⊥")

theorem Lean.Order.bot_le {α : Sort u} [CCPO α] (x : α) : PartialOrder.rel bot x

class Lean.Order.CompleteLattice (α : Sort u) extends Lean.Order.PartialOrder α : Sort (max 1 u)

A complete lattice is a partial order where every subset has a least upper bound.

• rel : α → α → Prop
• rel_refl {x : α} : rel x x
• rel_trans {x y z : α} : rel x y → rel y z → rel x z
• rel_antisymm {x y : α} : rel x y → rel y x → x = y
• has_sup (c : α → Prop) : Exists (is_sup c)

  The least upper bound of an arbitrary subset exists.

noncomputable def Lean.Order.CompleteLattice.sup {α : Sort u} [CompleteLattice α] (c : α → Prop) : α

Equations

• Lean.Order.CompleteLattice.sup c = Classical.choose ⋯

theorem Lean.Order.CompleteLattice.sup_spec {α : Sort u} [CompleteLattice α] (c : α → Prop) : is_sup c (sup c)

theorem Lean.Order.sup_le {α : Sort u} [CompleteLattice α] {x : α} (c : α → Prop) : (∀ (y : α), c y → PartialOrder.rel y x) → PartialOrder.rel (CompleteLattice.sup c) x

theorem Lean.Order.le_sup {α : Sort u} [CompleteLattice α] (c : α → Prop) {y : α} (hy : c y) : PartialOrder.rel y (CompleteLattice.sup c)

noncomputable def Lean.Order.inf {α : Sort u} [CompleteLattice α] (c : α → Prop) : α

Equations

• Lean.Order.inf c = Lean.Order.CompleteLattice.sup fun (x : α) => ∀ (y : α), c y → Lean.Order.PartialOrder.rel x y

theorem Lean.Order.inf_spec {α : Sort u} [CompleteLattice α] {x : α} {c : α → Prop} : PartialOrder.rel x (inf c) ↔ ∀ (y : α), c y → PartialOrder.rel x y

theorem Lean.Order.le_inf {α : Sort u} [CompleteLattice α] {x : α} {c : α → Prop} : (∀ (y : α), c y → PartialOrder.rel x y) → PartialOrder.rel x (inf c)

theorem Lean.Order.inf_le {α : Sort u} [CompleteLattice α] {c : α → Prop} {y : α} (hy : c y) : PartialOrder.rel (inf c) y

def Lean.Order.monotone {α : Sort u} [PartialOrder α] {β : Sort v} [PartialOrder β] (f : α → β) : Prop

A function is monotone if it maps related elements to related elements.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

Equations

• Lean.Order.monotone f = ∀ (x y : α), Lean.Order.PartialOrder.rel x y → Lean.Order.PartialOrder.rel (f x) (f y)

theorem Lean.Order.monotone_const {α : Sort u} [PartialOrder α] {β : Sort v} [PartialOrder β] (c : β) : monotone fun (x : α) => c

theorem Lean.Order.monotone_id {α : Sort u} [PartialOrder α] : monotone fun (x : α) => x

theorem Lean.Order.monotone_compose {α : Sort u} [PartialOrder α] {β : Sort v} [PartialOrder β] {γ : Sort w} [PartialOrder γ] {f : α → β} {g : β → γ} (hf : monotone f) (hg : monotone g) : monotone fun (x : α) => g (f x)

def Lean.Order.admissible {α : Sort u} [CCPO α] (P : α → Prop) : Prop

A predicate is admissible if it can be transferred from the elements of a chain to the chains least upper bound. Such predicates can be used in fixpoint induction.

This definition implies P ⊥. Sometimes (e.g. in Isabelle) the empty chain is excluded from this definition, and P ⊥ is a separate condition of the induction predicate.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

Equations

• Lean.Order.admissible P = ∀ (c : α → Prop) (hc : Lean.Order.chain c), (∀ (x : α), c x → P x) → P (Lean.Order.CCPO.csup hc)

theorem Lean.Order.admissible_const_true {α : Sort u} [CCPO α] : admissible fun (x : α) => True

theorem Lean.Order.admissible_and {α : Sort u} [CCPO α] (P Q : α → Prop) (hadm₁ : admissible P) (hadm₂ : admissible Q) : admissible fun (x : α) => P x ∧ Q x

theorem Lean.Order.chain_conj {α : Sort u} [CCPO α] (c P : α → Prop) (hchain : chain c) : chain fun (x : α) => c x ∧ P x

theorem Lean.Order.csup_conj {α : Sort u} [CCPO α] (c P : α → Prop) (hchain : chain c) (h : ∀ (x : α), c x → ∃ (y : α), c y ∧ PartialOrder.rel x y ∧ P y) : CCPO.csup hchain = CCPO.csup ⋯

theorem Lean.Order.admissible_or {α : Sort u} [CCPO α] (P Q : α → Prop) (hadm₁ : admissible P) (hadm₂ : admissible Q) : admissible fun (x : α) => P x ∨ Q x

theorem Lean.Order.admissible_pi {α : Sort u} [CCPO α] {β : Sort u_1} (P : α → β → Prop) (hadm₁ : ∀ (y : β), admissible fun (x : α) => P x y) : admissible fun (x : α) => ∀ (y : β), P x y

noncomputable def Lean.Order.lfp {α : Sort u} [CompleteLattice α] (f : α → α) : α

Equations

• Lean.Order.lfp f = Lean.Order.inf fun (c : α) => Lean.Order.PartialOrder.rel (f c) c

noncomputable def Lean.Order.lfp_monotone {α : Sort u} [CompleteLattice α] (f : α → α) (hm : monotone f) : α

Equations

• Lean.Order.lfp_monotone f hm = Lean.Order.lfp f

theorem Lean.Order.lfp_prefixed {α : Sort u} [CompleteLattice α] {f : α → α} {hm : monotone f} : PartialOrder.rel (f (lfp f)) (lfp f)

theorem Lean.Order.lfp_postfixed {α : Sort u} [CompleteLattice α] {f : α → α} {hm : monotone f} : PartialOrder.rel (lfp f) (f (lfp f))

theorem Lean.Order.lfp_fix {α : Sort u} [CompleteLattice α] {f : α → α} (hm : monotone f) : lfp f = f (lfp f)

theorem Lean.Order.lfp_monotone_fix {α : Sort u} [CompleteLattice α] {f : α → α} {hm : monotone f} : lfp_monotone f hm = f (lfp_monotone f hm)

theorem Lean.Order.lfp_le_of_le {α : Sort u} [CompleteLattice α] {x : α} {f : α → α} : PartialOrder.rel (f x) x → PartialOrder.rel (lfp f) x

Park induction principle for least fixpoint. In general, this construction does not require monotonicity of f. Monotonicity is required to show that lfp f is indeed a fixpoint of f.

theorem Lean.Order.lfp_le_of_le_monotone {α : Sort u} [CompleteLattice α] (f : α → α) {hm : monotone f} (x : α) : PartialOrder.rel (f x) x → PartialOrder.rel (lfp_monotone f hm) x

Park induction for least fixpoint of a monotone function f. Takes an explicit witness of f being monotone.

theorem Lean.Order.lfp_le_of_le_meet {α : Sort u} [CompleteLattice α] {f : α → α} (hm : monotone f) {x w : α} (hw : is_meet x (lfp f) w) (h : PartialOrder.rel (f w) x) : PartialOrder.rel (lfp f) x

Strong Park induction for the least fixpoint of a monotone function f: to show lfp f ⊑ x, it suffices to show f w ⊑ x where w is a greatest lower bound of x and lfp f. The meet is passed as an explicit witness w (together with a proof of is_meet x (lfp f) w) so that callers can supply a definitionally convenient form of it.

This is intended to be used in the construction of the strong induction principles of inductive_fixpoint and coinductive_fixpoint, and not meant to be used otherwise.

theorem Lean.Order.lfp_le_of_le_meet_monotone {α : Sort u} [CompleteLattice α] (f : α → α) {hm : monotone f} (x w : α) (hw : is_meet x (lfp_monotone f hm) w) : PartialOrder.rel (f w) x → PartialOrder.rel (lfp_monotone f hm) x

Same as lfp_le_of_le_meet, but uses the version of lfp that takes a witness of monotonicity.

This is intended to be used in the construction of the strong induction principles of inductive_fixpoint and coinductive_fixpoint, and not meant to be used otherwise.

inductive Lean.Order.iterates {α : Sort u} [CCPO α] (f : α → α) : α → Prop

The transfinite iteration of a function f is a set that is ⊥ and is closed under application of f and csup.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

• step {α : Sort u} [CCPO α] {f : α → α} {x : α} : iterates f x → iterates f (f x)
• sup {α : Sort u} [CCPO α] {f : α → α} {c : α → Prop} (hc : chain c) (hi : ∀ (x : α), c x → iterates f x) : iterates f (CCPO.csup hc)

theorem Lean.Order.chain_iterates {α : Sort u} [CCPO α] {f : α → α} (hf : monotone f) : chain (iterates f)

theorem Lean.Order.rel_f_of_iterates {α : Sort u} [CCPO α] {f : α → α} (hf : monotone f) {x : α} (hx : iterates f x) : PartialOrder.rel x (f x)

noncomputable def Lean.Order.fix {α : Sort u} [CCPO α] (f : α → α) (hmono : monotone f) : α

The least fixpoint of a monotone function is the least upper bound of its transfinite iteration.

The monotone f assumption is not strictly necessarily for the definition, but without this the definition is not very meaningful and it simplifies applying theorems like fix_eq if every use of fix already has the monotonicity requirement.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

Equations

• Lean.Order.fix f hmono = Lean.Order.CCPO.csup ⋯

theorem Lean.Order.fix_eq {α : Sort u} [CCPO α] {f : α → α} (hf : monotone f) : fix f hf = f (fix f hf)

The main fixpoint theorem for fixed points of monotone functions in chain-complete partial orders.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

theorem Lean.Order.fix_induct {α : Sort u} [CCPO α] {f : α → α} (hf : monotone f) (motive : α → Prop) (hadm : admissible motive) (h : ∀ (x : α), motive x → motive (f x)) : motive (fix f hf)

The fixpoint induction theme: An admissible predicate holds for a least fixpoint if it is preserved by the fixpoint's function.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

@[instance_reducible]

instance Lean.Order.instOrderPi {α : Sort u} {β : α → Sort v} [(x : α) → PartialOrder (β x)] : PartialOrder ((x : α) → β x)

Equations

• Lean.Order.instOrderPi = { rel := fun (f g : (x : α) → β x) => ∀ (x : α), Lean.Order.PartialOrder.rel (f x) (g x), rel_refl := ⋯, rel_trans := ⋯, rel_antisymm := ⋯ }

theorem Lean.Order.monotone_of_monotone_apply {α : Sort u} {β : α → Sort v} {γ : Sort w} [PartialOrder γ] [(x : α) → PartialOrder (β x)] (f : γ → (x : α) → β x) (h : ∀ (y : α), monotone fun (x : γ) => f x y) : monotone f

theorem Lean.Order.monotone_apply {α : Sort u} {β : α → Sort v} {γ : Sort w} [PartialOrder γ] [(x : α) → PartialOrder (β x)] (a : α) (f : γ → (x : α) → β x) (h : monotone f) : monotone fun (x : γ) => f x a

theorem Lean.Order.is_meet_pi {α : Sort u} {β : α → Sort v} [(x : α) → PartialOrder (β x)] {f g w : (x : α) → β x} (h : ∀ (x : α), is_meet (f x) (g x) (w x)) : is_meet f g w

A pointwise greatest lower bound is a greatest lower bound in the pointwise order.

theorem Lean.Order.chain_apply {α : Sort u} {β : α → Sort v} [(x : α) → PartialOrder (β x)] {c : ((x : α) → β x) → Prop} (hc : chain c) (x : α) : chain fun (y : β x) => ∃ (f : (x : α) → β x), c f ∧ f x = y

noncomputable def Lean.Order.fun_csup {α : Sort u} {β : α → Sort v} [(x : α) → CCPO (β x)] (c : ((x : α) → β x) → Prop) (hc : chain c) (x : α) : β x

Equations

• Lean.Order.fun_csup c hc x = Lean.Order.CCPO.csup ⋯

theorem Lean.Order.fun_csup_is_sup {α : Sort u} {β : α → Sort v} [(x : α) → CCPO (β x)] (c : ((x : α) → β x) → Prop) (hc : chain c) : is_sup c (fun_csup c hc)

@[instance_reducible]

instance Lean.Order.instCCPOPi {α : Sort u} {β : α → Sort v} [(x : α) → CCPO (β x)] : CCPO ((x : α) → β x)

Equations

• Lean.Order.instCCPOPi = { toPartialOrder := Lean.Order.instOrderPi, has_csup := ⋯ }

theorem Lean.Order.fun_csup_eq {α : Sort u} {β : α → Sort v} [(x : α) → CCPO (β x)] (c : ((x : α) → β x) → Prop) (hc : chain c) : fun_csup c hc = CCPO.csup hc

noncomputable def Lean.Order.fun_sup {α : Sort u} {β : α → Sort v} [(x : α) → CompleteLattice (β x)] (c : ((x : α) → β x) → Prop) (x : α) : β x

Equations

• Lean.Order.fun_sup c x = Lean.Order.CompleteLattice.sup fun (y : β x) => ∃ (f : (x : α) → β x), c f ∧ f x = y

theorem Lean.Order.fun_sup_is_sup {α : Sort u} {β : α → Sort v} [(x : α) → CompleteLattice (β x)] (c : ((x : α) → β x) → Prop) : is_sup c (fun_sup c)

@[instance_reducible]

instance Lean.Order.instCompleteLatticePi {α : Sort u} {β : α → Sort v} [(x : α) → CompleteLattice (β x)] : CompleteLattice ((x : α) → β x)

Equations

• Lean.Order.instCompleteLatticePi = { toPartialOrder := Lean.Order.instOrderPi, has_sup := ⋯ }

theorem Lean.Order.fun_sup_eq {α : Sort u} {β : α → Sort v} [(x : α) → CompleteLattice (β x)] (c : ((x : α) → β x) → Prop) : fun_sup c = CompleteLattice.sup c

theorem Lean.Order.admissible_apply {α : Sort u} {β : α → Sort v} [(x : α) → CCPO (β x)] (P : (x : α) → β x → Prop) (x : α) (hadm : admissible (P x)) : admissible fun (f : (x : α) → β x) => P x (f x)

theorem Lean.Order.admissible_pi_apply {α : Sort u} {β : α → Sort v} [(x : α) → CCPO (β x)] (P : (x : α) → β x → Prop) (hadm : ∀ (x : α), admissible (P x)) : admissible fun (f : (x : α) → β x) => ∀ (x : α), P x (f x)

theorem Lean.Order.monotone_ite {α : Sort u} {β : Sort v} [PartialOrder α] [PartialOrder β] (c : Prop) [Decidable c] (k₁ k₂ : α → β) (hmono₁ : monotone k₁) (hmono₂ : monotone k₂) : monotone fun (x : α) => if c then k₁ x else k₂ x

theorem Lean.Order.monotone_dite {α : Sort u} {β : Sort v} [PartialOrder α] [PartialOrder β] (c : Prop) [Decidable c] (k₁ : α → c → β) (k₂ : α → ¬c → β) (hmono₁ : monotone k₁) (hmono₂ : monotone k₂) : monotone fun (x : α) => dite c (k₁ x) (k₂ x)

@[instance_reducible]

instance Lean.Order.instPartialOrderPProd {α : Sort u} {β : Sort v} [PartialOrder α] [PartialOrder β] : PartialOrder (α ×' β)

Equations

• One or more equations did not get rendered due to their size.

theorem Lean.Order.is_meet_pprod {α : Sort u} {β : Sort v} [PartialOrder α] [PartialOrder β] {x y w : α ×' β} (h₁ : is_meet x.fst y.fst w.fst) (h₂ : is_meet x.snd y.snd w.snd) : is_meet x y w

A componentwise greatest lower bound is a greatest lower bound in the product order.

theorem Lean.Order.PProd.monotone_mk {α : Sort u} {β : Sort v} {γ : Sort w} [PartialOrder α] [PartialOrder β] [PartialOrder γ] {f : γ → α} {g : γ → β} (hf : monotone f) (hg : monotone g) : monotone fun (x : γ) => ⟨f x, g x⟩

theorem Lean.Order.PProd.monotone_fst {α : Sort u} {β : Sort v} {γ : Sort w} [PartialOrder α] [PartialOrder β] [PartialOrder γ] {f : γ → α ×' β} (hf : monotone f) : monotone fun (x : γ) => (f x).fst

theorem Lean.Order.PProd.monotone_snd {α : Sort u} {β : Sort v} {γ : Sort w} [PartialOrder α] [PartialOrder β] [PartialOrder γ] {f : γ → α ×' β} (hf : monotone f) : monotone fun (x : γ) => (f x).snd

def Lean.Order.PProd.chain.fst {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (c : α ×' β → Prop) : α → Prop

Equations

• Lean.Order.PProd.chain.fst c a = ∃ (b : β), c ⟨a, b⟩

def Lean.Order.PProd.chain.snd {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (c : α ×' β → Prop) : β → Prop

Equations

• Lean.Order.PProd.chain.snd c b = ∃ (a : α), c ⟨a, b⟩

def Lean.Order.PProd.fst {α : Sort u} {β : Sort v} [CompleteLattice α] [CompleteLattice β] (c : α ×' β → Prop) : α → Prop

Equations

• Lean.Order.PProd.fst c a = ∃ (b : β), c ⟨a, b⟩

def Lean.Order.PProd.snd {α : Sort u} {β : Sort v} [CompleteLattice α] [CompleteLattice β] (c : α ×' β → Prop) : β → Prop

Equations

• Lean.Order.PProd.snd c b = ∃ (a : α), c ⟨a, b⟩

theorem Lean.Order.PProd.chain.chain_fst {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] {c : α ×' β → Prop} (hchain : chain c) : chain (fst c)

theorem Lean.Order.PProd.chain.chain_snd {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] {c : α ×' β → Prop} (hchain : chain c) : chain (snd c)

noncomputable def Lean.Order.prod_csup {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (c : α ×' β → Prop) (hchain : chain c) : α ×' β

Equations

• Lean.Order.prod_csup c hchain = ⟨Lean.Order.CCPO.csup ⋯, Lean.Order.CCPO.csup ⋯⟩

theorem Lean.Order.prod_csup_is_sup {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (c : α ×' β → Prop) (hchain : chain c) : is_sup c (prod_csup c hchain)

@[instance_reducible]

instance Lean.Order.instCCPOPProd {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] : CCPO (α ×' β)

Equations

• Lean.Order.instCCPOPProd = { toPartialOrder := Lean.Order.instPartialOrderPProd, has_csup := ⋯ }

theorem Lean.Order.prod_csup_eq {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (c : α ×' β → Prop) (hchain : chain c) : prod_csup c hchain = CCPO.csup hchain

noncomputable def Lean.Order.prod_sup {α : Sort u} {β : Sort v} [CompleteLattice α] [CompleteLattice β] (c : α ×' β → Prop) : α ×' β

Equations

• Lean.Order.prod_sup c = ⟨Lean.Order.CompleteLattice.sup (Lean.Order.PProd.fst c), Lean.Order.CompleteLattice.sup (Lean.Order.PProd.snd c)⟩

theorem Lean.Order.prod_sup_is_sup {α : Sort u} {β : Sort v} [CompleteLattice α] [CompleteLattice β] (c : α ×' β → Prop) : is_sup c (prod_sup c)

@[instance_reducible]

instance Lean.Order.instCompleteLatticePProd {α : Sort u} {β : Sort v} [CompleteLattice α] [CompleteLattice β] : CompleteLattice (α ×' β)

Equations

• Lean.Order.instCompleteLatticePProd = { toPartialOrder := Lean.Order.instPartialOrderPProd, has_sup := ⋯ }

theorem Lean.Order.admissible_pprod_fst {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (P : α → Prop) (hadm : admissible P) : admissible fun (x : α ×' β) => P x.fst

theorem Lean.Order.admissible_pprod_snd {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (P : β → Prop) (hadm : admissible P) : admissible fun (x : α ×' β) => P x.snd

@[instance_reducible]

instance Lean.Order.instPartialOrderProd {α : Type u} {β : Type v} [PartialOrder α] [PartialOrder β] : PartialOrder (α × β)

The order on α × β is the order on α ×' β at the two components.

Equations

• Lean.Order.instPartialOrderProd = { rel := fun (a b : α × β) => Lean.Order.PartialOrder.rel ⟨a.fst, a.snd⟩ ⟨b.fst, b.snd⟩, rel_refl := ⋯, rel_trans := ⋯, rel_antisymm := ⋯ }

theorem Lean.Order.Prod.mk_le {α : Type u} {β : Type v} [PartialOrder α] [PartialOrder β] (a : α) (b : β) (p : α × β) (ha : PartialOrder.rel a p.fst) (hb : PartialOrder.rel b p.snd) : PartialOrder.rel (a, b) p

A pair is below p when both components are below the components of p.

theorem Lean.Order.Prod.mk_le_snd {α : Type u} {β : Type v} [PartialOrder α] [PartialOrder β] (b : β) (p : α × β) (hb : PartialOrder.rel b p.snd) : PartialOrder.rel (p.fst, b) p

A pair with the first component of p is below p when its second component is below the second component of p.

theorem Lean.Order.Prod.is_sup_of_pprod {α : Type u} {β : Type v} [PartialOrder α] [PartialOrder β] {c : α × β → Prop} {s : α ×' β} (h : is_sup (fun (p : α ×' β) => c (p.fst, p.snd)) s) : is_sup c (s.fst, s.snd)

A least upper bound of the pairs of c in α ×' β is one in α × β.

@[instance_reducible]

instance Lean.Order.instCCPOProd {α : Type u} {β : Type v} [CCPO α] [CCPO β] : CCPO (α × β)

The chain-complete suprema of α × β are those of α ×' β at the two components.

Equations

• Lean.Order.instCCPOProd = { toPartialOrder := Lean.Order.instPartialOrderProd, has_csup := ⋯ }

@[instance_reducible]

instance Lean.Order.instCompleteLatticeProd {α : Type u} {β : Type v} [CompleteLattice α] [CompleteLattice β] : CompleteLattice (α × β)

The suprema of α × β are those of α ×' β at the two components.

Equations

• Lean.Order.instCompleteLatticeProd = { toPartialOrder := Lean.Order.instPartialOrderProd, has_sup := ⋯ }

@[instance_reducible]

instance Lean.Order.instPartialOrderUnit : PartialOrder Unit

Equations

• Lean.Order.instPartialOrderUnit = { rel := fun (x x_1 : Unit) => True, rel_refl := ⋯, rel_trans := ⋯, rel_antisymm := ⋯ }

theorem Lean.Order.Unit.unit_le (u : Unit) : PartialOrder.rel () u

The unique Unit value is below every Unit value.

@[instance_reducible]

instance Lean.Order.instCCPOUnit : CCPO Unit

Equations

• Lean.Order.instCCPOUnit = { toPartialOrder := Lean.Order.instPartialOrderUnit, has_csup := @Lean.Order.instCCPOUnit._proof_1 }

@[instance_reducible]

instance Lean.Order.instCompleteLatticeUnit : CompleteLattice Unit

Equations

• Lean.Order.instCompleteLatticeUnit = { toPartialOrder := Lean.Order.instPartialOrderUnit, has_sup := Lean.Order.instCompleteLatticeUnit._proof_1 }

def Lean.Order.FlatOrder {α : Sort u} (b : α) : Sort u

FlatOrder b wraps the type α with the flat partial order generated by ∀ x, b ⊑ x.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

Equations

• Lean.Order.FlatOrder b = α

def Lean.Order.FlatOrder.mk {α : Sort u} (b x : α) : FlatOrder b

Equations

• Lean.Order.FlatOrder.mk b x = x

def Lean.Order.FlatOrder.inner {α : Sort u} {b : α} (x : FlatOrder b) : α

Equations

• x.inner = x

theorem Lean.Order.FlatOrder.mk_inner {α : Sort u} {b : α} {x : FlatOrder b} : mk b x.inner = x

theorem Lean.Order.FlatOrder.inner_mk {α : Sort u} {b x : α} : (mk b x).inner = x

@[simp]

theorem Lean.Order.FlatOrder.mk_inj {α : Sort u} {b x y : α} : mk b x = mk b y ↔ x = y

inductive Lean.Order.FlatOrder.rel {α : Sort u} {b : α} (x y : FlatOrder b) : Prop

The flat partial order generated by ∀ x, b ⊑ x.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

• bot {α : Sort u} {b : α} {x : FlatOrder b} : rel b x
• refl {α : Sort u} {b : α} {x : FlatOrder b} : x.rel x

@[instance_reducible]

instance Lean.Order.FlatOrder.instOrder {α : Sort u} {b : α} : PartialOrder (FlatOrder b)

Equations

• Lean.Order.FlatOrder.instOrder = { rel := Lean.Order.FlatOrder.rel, rel_refl := ⋯, rel_trans := ⋯, rel_antisymm := ⋯ }

noncomputable def Lean.Order.flat_csup {α : Sort u} {b : α} (c : FlatOrder b → Prop) : FlatOrder b

Equations

• Lean.Order.flat_csup c = if h : ∃ (x : Lean.Order.FlatOrder b), c x ∧ x ≠ b then Classical.choose h else Lean.Order.FlatOrder.mk b b

theorem Lean.Order.flat_csup_is_sup {α : Sort u} {b : α} (c : FlatOrder b → Prop) (hc : chain c) : is_sup c (flat_csup c)

@[instance_reducible]

instance Lean.Order.FlatOrder.instCCPO {α : Sort u} {b : α} : CCPO (FlatOrder b)

Equations

• Lean.Order.FlatOrder.instCCPO = { toPartialOrder := Lean.Order.FlatOrder.instOrder, has_csup := ⋯ }

theorem Lean.Order.flat_csup_eq {α : Sort u} {b : α} (c : FlatOrder b → Prop) (hchain : chain c) : flat_csup c = CCPO.csup hchain

theorem Lean.Order.admissible_flatOrder {α : Sort u} {b : α} (P : FlatOrder b → Prop) (hnot : P (FlatOrder.mk b b)) : admissible P

class Lean.Order.MonoBind (m : Type u → Type v) [Bind m] [(α : Type u) → PartialOrder (m α)] : Prop

The class MonoBind m indicates that every m α has a PartialOrder, and that the bind operation on m is monotone in both arguments with regard to that order.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

• bind_mono_left {α β : Type u} {a₁ a₂ : m α} {f : α → m β} (h : PartialOrder.rel a₁ a₂) : PartialOrder.rel (a₁ >>= f) (a₂ >>= f)
• bind_mono_right {α β : Type u} {a : m α} {f₁ f₂ : α → m β} (h : ∀ (x : α), PartialOrder.rel (f₁ x) (f₂ x)) : PartialOrder.rel (a >>= f₁) (a >>= f₂)

theorem Lean.Order.monotone_bind (m : Type u → Type v) [Bind m] [(α : Type u) → PartialOrder (m α)] [MonoBind m] {α β : Type u} {γ : Sort w} [PartialOrder γ] (f : γ → m α) (g : γ → α → m β) (hmono₁ : monotone f) (hmono₂ : monotone g) : monotone fun (x : γ) => f x >>= g x

@[instance_reducible]

instance Lean.Order.instPartialOrderOption {α : Type u_1} : PartialOrder (Option α)

Equations

• Lean.Order.instPartialOrderOption = { rel := Lean.Order.instPartialOrderOption._aux_1, rel_refl := ⋯, rel_trans := ⋯, rel_antisymm := ⋯ }

@[instance_reducible]

instance Lean.Order.instCCPOOption {α : Type u_1} : CCPO (Option α)

Equations

• Lean.Order.instCCPOOption = { toPartialOrder := Lean.Order.instPartialOrderOption, has_csup := ⋯ }

instance Lean.Order.instMonoBindOption : MonoBind Option

theorem Lean.Order.Option.admissible_eq_some {α : Type u_1} (P : Prop) (y : α) : admissible fun (x : Option α) => x = some y → P

@[instance_reducible]

instance Lean.Order.instPartialOrderExceptT {m : Type u_1 → Type u_2} {ε α : Type u_1} [inst : (α : Type u_1) → PartialOrder (m α)] : PartialOrder (ExceptT ε m α)

Equations

• Lean.Order.instPartialOrderExceptT = inst (Except ε α)

@[instance_reducible]

instance Lean.Order.instCCPOExceptT {m : Type u_1 → Type u_2} {ε α : Type u_1} [inst : (α : Type u_1) → CCPO (m α)] : CCPO (ExceptT ε m α)

Equations

• Lean.Order.instCCPOExceptT = inst (Except ε α)

instance Lean.Order.instMonoBindExceptT {m : Type u_1 → Type u_2} {ε : Type u_1} [Monad m] [(α : Type u_1) → PartialOrder (m α)] [MonoBind m] : MonoBind (ExceptT ε m)

theorem Lean.Order.monotone_exceptTRun {γ : Sort u_1} {m : Type u_2 → Type u_3} {ε α : Type u_2} [PartialOrder γ] [Monad m] [(α : Type u_2) → PartialOrder (m α)] (f : γ → ExceptT ε m α) (hmono : monotone f) : monotone fun (x : γ) => (f x).run

@[instance_reducible]

instance Lean.Order.instPartialOrderOptionT {m : Type u_1 → Type u_2} {α : Type u_1} [inst : (α : Type u_1) → PartialOrder (m α)] : PartialOrder (OptionT m α)

Equations

• Lean.Order.instPartialOrderOptionT = inst (Option α)

@[instance_reducible]

instance Lean.Order.instCCPOOptionT {m : Type u_1 → Type u_2} {α : Type u_1} [inst : (α : Type u_1) → CCPO (m α)] : CCPO (OptionT m α)

Equations

• Lean.Order.instCCPOOptionT = inst (Option α)

instance Lean.Order.instMonoBindOptionT {m : Type u_1 → Type u_2} [Monad m] [(α : Type u_1) → PartialOrder (m α)] [MonoBind m] : MonoBind (OptionT m)

theorem Lean.Order.monotone_optionTRun {γ : Sort u_1} {m : Type u_2 → Type u_3} {α : Type u_2} [PartialOrder γ] [Monad m] [(α : Type u_2) → PartialOrder (m α)] (f : γ → OptionT m α) (hmono : monotone f) : monotone fun (x : γ) => (f x).run

@[instance_reducible]

instance Lean.Order.instPartialOrderReaderT {m : Type u_1 → Type u_2} {ρ α : Type u_1} [inst : PartialOrder (m α)] : PartialOrder (ReaderT ρ m α)

Equations

• Lean.Order.instPartialOrderReaderT = Lean.Order.instOrderPi

@[instance_reducible]

instance Lean.Order.instCCPOReaderT {m : Type u_1 → Type u_2} {ρ α : Type u_1} [inst : CCPO (m α)] : CCPO (ReaderT ρ m α)

Equations

• Lean.Order.instCCPOReaderT = Lean.Order.instCCPOPi

instance Lean.Order.instMonoBindReaderT {m : Type u_1 → Type u_2} {ρ : Type u_1} [Monad m] [(α : Type u_1) → PartialOrder (m α)] [MonoBind m] : MonoBind (ReaderT ρ m)

theorem Lean.Order.monotone_readerTRun {γ : Sort u_1} {m : Type u_2 → Type u_3} {α σ : Type u_2} [PartialOrder γ] [Monad m] [PartialOrder (m α)] (f : γ → ReaderT σ m α) (hmono : monotone f) (s : σ) : monotone fun (x : γ) => (f x).run s

@[instance_reducible]

instance Lean.Order.instPartialOrderStateRefT' {m : Type → Type} {ω σ α : Type} [inst : PartialOrder (m α)] : PartialOrder (StateRefT' ω σ m α)

Equations

• Lean.Order.instPartialOrderStateRefT' = Lean.Order.instOrderPi

@[instance_reducible]

instance Lean.Order.instCCPOStateRefT' {m : Type → Type} {ω σ α : Type} [inst : CCPO (m α)] : CCPO (StateRefT' ω σ m α)

Equations

• Lean.Order.instCCPOStateRefT' = Lean.Order.instCCPOPi

instance Lean.Order.instMonoBindStateRefT' {m : Type → Type} {ω σ : Type} [Monad m] [(α : Type) → PartialOrder (m α)] [MonoBind m] : MonoBind (StateRefT' ω σ m)

theorem Lean.Order.monotone_stateRefT'Run {γ : Sort u_1} {m : Type → Type} {ω σ α : Type} [PartialOrder γ] [Monad m] [MonadLiftT (ST ω) m] [(α : Type) → PartialOrder (m α)] [MonoBind m] (f : γ → StateRefT' ω σ m α) (hmono : monotone f) (s : σ) : monotone fun (x : γ) => (f x).run s

@[instance_reducible]

instance Lean.Order.instPartialOrderStateT {m : Type u_1 → Type u_2} {σ α : Type u_1} [inst : (α : Type u_1) → PartialOrder (m α)] : PartialOrder (StateT σ m α)

Equations

• Lean.Order.instPartialOrderStateT = Lean.Order.instOrderPi

@[instance_reducible]

instance Lean.Order.instCCPOStateT {m : Type u_1 → Type u_2} {σ α : Type u_1} [inst : (α : Type u_1) → CCPO (m α)] : CCPO (StateT σ m α)

Equations

• Lean.Order.instCCPOStateT = Lean.Order.instCCPOPi

instance Lean.Order.instMonoBindStateT {m : Type u_1 → Type u_2} {ρ : Type u_1} [Monad m] [(α : Type u_1) → PartialOrder (m α)] [MonoBind m] : MonoBind (StateT ρ m)

theorem Lean.Order.monotone_stateTRun {γ : Sort u_1} {m : Type u_2 → Type u_3} {σ α : Type u_2} [PartialOrder γ] [Monad m] [(α : Type u_2) → PartialOrder (m α)] (f : γ → StateT σ m α) (hmono : monotone f) (s : σ) : monotone fun (x : γ) => (f x).run s

noncomputable def Lean.Order.EST.bot {ε σ α : Type} [Nonempty ε] : EST ε σ α

Equations

• Lean.Order.EST.bot s = EST.Out.error Classical.ofNonempty (Classical.choice ⋯)

@[instance_reducible]

instance Lean.Order.instCCPOESTOfNonempty {ε σ α : Type} [Nonempty ε] : CCPO (EST ε σ α)

Equations

• Lean.Order.instCCPOESTOfNonempty = { rel := Lean.Order.PartialOrder.rel, rel_refl := ⋯, rel_trans := ⋯, rel_antisymm := ⋯, has_csup := ⋯ }

instance Lean.Order.instMonoBindEST {ε σ : Type} [Nonempty ε] : MonoBind (EST ε σ)

@[instance_reducible]

instance Lean.Order.instCCPOEIOOfNonempty {ε α : Type} [Nonempty ε] : CCPO (EIO ε α)

Equations

• Lean.Order.instCCPOEIOOfNonempty = { rel := Lean.Order.instCCPOEIOOfNonempty._aux_1, rel_refl := ⋯, rel_trans := ⋯, rel_antisymm := ⋯, has_csup := ⋯ }

instance Lean.Order.instMonoBindEIO {ε : Type} [Nonempty ε] : MonoBind (EIO ε)

@[instance_reducible]

instance Lean.Order.instCCPOIO {α : Type} : CCPO (IO α)

Equations

• Lean.Order.instCCPOIO = { toPartialOrder := Lean.Order.instCCPOEIOOfNonempty.toPartialOrder, has_csup := ⋯ }

instance Lean.Order.instMonoBindIO : MonoBind IO

def Lean.Order.ImplicationOrder : Type

Equations

• Lean.Order.ImplicationOrder = Prop

@[instance_reducible]

instance Lean.Order.ImplicationOrder.instOrder : PartialOrder ImplicationOrder

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Lean.Order.ImplicationOrder.instCompleteLattice : CompleteLattice ImplicationOrder

Equations

• Lean.Order.ImplicationOrder.instCompleteLattice = { toPartialOrder := Lean.Order.ImplicationOrder.instOrder, has_sup := ⋯ }

theorem Lean.Order.implication_order_monotone_exists {α : Sort u_1} [PartialOrder α] {β : Sort u_2} (f : α → β → ImplicationOrder) (h : monotone f) : monotone fun (x : α) => Exists (f x)

theorem Lean.Order.implication_order_monotone_forall {α : Sort u_1} [PartialOrder α] {β : Sort u_2} (f : α → β → ImplicationOrder) (h : monotone f) : monotone fun (x : α) => ∀ (y : β), f x y

theorem Lean.Order.implication_order_monotone_and {α : Sort u_1} [PartialOrder α] (f₁ f₂ : α → ImplicationOrder) (h₁ : monotone f₁) (h₂ : monotone f₂) : monotone fun (x : α) => f₁ x ∧ f₂ x

theorem Lean.Order.implication_order_monotone_or {α : Sort u_1} [PartialOrder α] (f₁ f₂ : α → ImplicationOrder) (h₁ : monotone f₁) (h₂ : monotone f₂) : monotone fun (x : α) => f₁ x ∨ f₂ x

theorem Lean.Order.ImplicationOrder.is_meet_and (x y : ImplicationOrder) : is_meet x y (x ∧ y)

In the implication order the meet of two propositions is their conjunction.

def Lean.Order.ReverseImplicationOrder : Type

Equations

• Lean.Order.ReverseImplicationOrder = Prop

@[instance_reducible]

instance Lean.Order.ReverseImplicationOrder.instOrder : PartialOrder ReverseImplicationOrder

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Lean.Order.ReverseImplicationOrder.instCompleteLattice : CompleteLattice ReverseImplicationOrder

Equations

• Lean.Order.ReverseImplicationOrder.instCompleteLattice = { toPartialOrder := Lean.Order.ReverseImplicationOrder.instOrder, has_sup := ⋯ }

theorem Lean.Order.coind_monotone_exists {α : Sort u_1} [PartialOrder α] {β : Sort u_2} (f : α → β → ReverseImplicationOrder) (h : monotone f) : monotone fun (x : α) => Exists (f x)

theorem Lean.Order.coind_monotone_forall {α : Sort u_1} [PartialOrder α] {β : Sort u_2} (f : α → β → ReverseImplicationOrder) (h : monotone f) : monotone fun (x : α) => ∀ (y : β), f x y

theorem Lean.Order.coind_monotone_and {α : Sort u_1} [PartialOrder α] (f₁ f₂ : α → Prop) (h₁ : monotone f₁) (h₂ : monotone f₂) : monotone fun (x : α) => f₁ x ∧ f₂ x

theorem Lean.Order.coind_monotone_or {α : Sort u_1} [PartialOrder α] (f₁ f₂ : α → Prop) (h₁ : monotone f₁) (h₂ : monotone f₂) : monotone fun (x : α) => f₁ x ∨ f₂ x

theorem Lean.Order.ReverseImplicationOrder.is_meet_or (x y : ReverseImplicationOrder) : is_meet x y (x ∨ y)

In the reverse implication order the meet of two propositions is their disjunction.

theorem Lean.Order.coind_not {α : Sort u_1} [PartialOrder α] (f₁ : α → Prop) (h₁ : monotone f₁) : monotone fun (x : α) => ¬f₁ x

theorem Lean.Order.ind_not {α : Sort u_1} [PartialOrder α] (f₁ : α → Prop) (h₁ : monotone f₁) : monotone fun (x : α) => ¬f₁ x

theorem Lean.Order.ind_impl {α : Sort u_1} [PartialOrder α] (f₁ f₂ : α → Prop) (h₁ : monotone f₁) (h₂ : monotone f₂) : monotone fun (x : α) => f₁ x → f₂ x

theorem Lean.Order.coind_impl {α : Sort u_1} [PartialOrder α] (f₁ f₂ : α → Prop) (h₁ : monotone f₁) (h₂ : monotone f₂) : monotone fun (x : α) => f₁ x → f₂ x

def Lean.Order.Example.findF (P : Nat → Bool) (rec : Nat → Option Nat) (x : Nat) : Option Nat

Equations

• Lean.Order.Example.findF P rec x = if P x = true then some x else rec (x + 1)

noncomputable def Lean.Order.Example.find (P : Nat → Bool) : Nat → Option Nat

Equations

• Lean.Order.Example.find P = Lean.Order.fix (Lean.Order.Example.findF P) ⋯

theorem Lean.Order.Example.find_eq {P : Nat → Bool} : find P = findF P (find P)

theorem Lean.Order.Example.find_spec {P : Nat → Bool} (n m : Nat) : find P n = some m → n ≤ m ∧ P m = true