Documentation

Init.WF

source
inductive Acc {α : Sort u} (r : α → α → Prop) :
α → Prop
  • intro: ∀ {α : Sort u} {r : α → α → Prop} (x : α), (∀ (y : α), r y x → Acc r y) → Acc r x
source
@[inline]
abbrev Acc.ndrec {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1} (m : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → C y) → C x) {a : α} (n : Acc r a) :
C a
Equations
source
@[inline]
abbrev Acc.ndrecOn {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1} {a : α} (n : Acc r a) (m : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → C y) → C x) :
C a
Equations
source
def Acc.inv {α : Sort u} {r : α → α → Prop} {x : α} {y : α} (h₁ : Acc r x) (h₂ : r y x) :
Acc r y
Equations
source
inductive WellFounded {α : Sort u} (r : α → α → Prop) :
Prop
  • intro: ∀ {α : Sort u} {r : α → α → Prop}, (∀ (a : α), Acc r a) → WellFounded r
source
class WellFoundedRelation (α : Sort u) :
Sort (max 1 u)
Instances
source
def WellFounded.apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) :
Acc r a
Equations
source
theorem WellFounded.recursion {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r) {C : α → Sort v} (a : α) (h : (x : α) → ((y : α) → r y x → C y) → C x) :
C a
source
theorem WellFounded.induction {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r) {C : α → Prop} (a : α) (h : (x : α) → ((y : α) → r y x → C y) → C x) :
C a
source
def WellFounded.fixF {α : Sort u} {r : α → α → Prop} {C : α → Sort v} (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) (a : Acc r x) :
C x
Equations
source
def WellFounded.fixFEq {α : Sort u} {r : α → α → Prop} {C : α → Sort v} (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) (acx : Acc r x) :
WellFounded.fixF F x acx = F x fun y p => WellFounded.fixF F y (_ : Acc (fun y x => r y x) y)
Equations
source
def WellFounded.fix {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : WellFounded r) (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) :
C x
Equations
source
theorem WellFounded.fix_eq {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : WellFounded r) (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) :
WellFounded.fix hwf F x = F x fun y x => WellFounded.fix hwf F y
source
def emptyWf {α : Sort u} :
WellFoundedRelation α
Equations
  • emptyWf = { rel := emptyRelation, wf := (_ : WellFounded emptyRelation) }
source
def Subrelation.accessible {α : Sort u} {r : α → α → Prop} {q : α → α → Prop} {a : α} (h₁ : Subrelation q r) (ac : Acc r a) :
Acc q a
Equations
source
def Subrelation.wf {α : Sort u} {r : α → α → Prop} {q : α → α → Prop} (h₁ : Subrelation q r) (h₂ : WellFounded r) :
WellFounded q
Equations
source
def InvImage.accessible {α : Sort u} {β : Sort v} {r : β → β → Prop} {a : α} (f : α → β) (ac : Acc r (f a)) :
Acc (InvImage r f) a
Equations
source
def InvImage.wf {α : Sort u} {β : Sort v} {r : β → β → Prop} (f : α → β) (h : WellFounded r) :
WellFounded (InvImage r f)
Equations
source
def invImage {α : Sort u_1} {β : Sort u_2} (f : α → β) (h : WellFoundedRelation β) :
WellFoundedRelation α
Equations
source
def TC.accessible {α : Sort u} {r : α → α → Prop} {z : α} (ac : Acc r z) :
Acc (TC r) z
Equations
source
def TC.wf {α : Sort u} {r : α → α → Prop} (h : WellFounded r) :
WellFounded (TC r)
Equations
source
def Nat.lt_wfRel:
WellFoundedRelation Nat
Equations
source
theorem Nat.strongInductionOn {motive : Nat → Sort u} (n : Nat) (ind : (n : Nat) → ((m : Nat) → m < n → motive m) → motive n) :
motive n
source
theorem Nat.caseStrongInductionOn {motive : Nat → Sort u} (a : Nat) (zero : motive 0) (ind : (n : Nat) → ((m : Nat) → m ≤ n → motive m) → motive (Nat.succ n)) :
motive a
source
def Measure {α : Sort u} :
(α → Nat) → α → α → Prop
Equations
source
@[inline]
abbrev measure {α : Sort u} (f : α → Nat) :
WellFoundedRelation α
Equations
source
def SizeOfRef (α : Sort u) [inst : SizeOf α] :
α → α → Prop
Equations
source
@[inline]
abbrev sizeOfWFRel {α : Sort u} [inst : SizeOf α] :
WellFoundedRelation α
Equations
source
instance instWellFoundedRelation {α : Sort u_1} [inst : SizeOf α] :
WellFoundedRelation α
Equations
  • instWellFoundedRelation = sizeOfWFRel
source
inductive Prod.Lex {α : Type u} {β : Type v} (ra : α → α → Prop) (rb : β → β → Prop) :
α × β → α × β → Prop
  • left: ∀ {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} {a₁ : α} (b₁ : β) {a₂ : α} (b₂ : β), ra a₁ a₂ → Prod.Lex ra rb (a₁, b₁) (a₂, b₂)
  • right: ∀ {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (a : α) {b₁ b₂ : β}, rb b₁ b₂ → Prod.Lex ra rb (a, b₁) (a, b₂)
source
def Prod.Lex.right' {β : Type v} (rb : β → β → Prop) {a₂ : Nat} {b₂ : β} {a₁ : Nat} {b₁ : β} (h₁ : a₁ ≤ a₂) (h₂ : rb b₁ b₂) :
Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂)
Equations
source
inductive Prod.RProd {α : Type u} {β : Type v} (ra : α → α → Prop) (rb : β → β → Prop) :
α × β → α × β → Prop
  • intro: ∀ {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} {a₁ : α} {b₁ : β} {a₂ : α} {b₂ : β}, ra a₁ a₂ → rb b₁ b₂ → Prod.RProd ra rb (a₁, b₁) (a₂, b₂)
source
def Prod.lexAccessible {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (aca : ∀ (a : α), Acc ra a) (acb : ∀ (b : β), Acc rb b) (a : α) (b : β) :
Acc (Prod.Lex ra rb) (a, b)
Equations
source
def Prod.lex {α : Type u} {β : Type v} (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) :
WellFoundedRelation (α × β)
Equations
source
instance Prod.instWellFoundedRelationProd {α : Type u} {β : Type v} [ha : WellFoundedRelation α] [hb : WellFoundedRelation β] :
WellFoundedRelation (α × β)
Equations
  • Prod.instWellFoundedRelationProd = Prod.lex ha hb
source
def Prod.RProdSubLex {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (a : α × β) (b : α × β) (h : Prod.RProd ra rb a b) :
Prod.Lex ra rb a b
Equations
source
def Prod.rprod {α : Type u} {β : Type v} (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) :
WellFoundedRelation (α × β)
Equations
source
inductive PSigma.Lex {α : Sort u} {β : α → Sort v} (r : α → α → Prop) (s : (a : α) → β a → β a → Prop) :
PSigma β → PSigma β → Prop
  • left: ∀ {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop} {a₁ : α} (b₁ : β a₁) {a₂ : α} (b₂ : β a₂), r a₁ a₂ → PSigma.Lex r s { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ }
  • right: ∀ {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop} (a : α) {b₁ b₂ : β a}, s a b₁ b₂ → PSigma.Lex r s { fst := a, snd := b₁ } { fst := a, snd := b₂ }
source
def PSigma.lexAccessible {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop} {a : α} (aca : Acc r a) (acb : ∀ (a : α), WellFounded (s a)) (b : β a) :
Acc (PSigma.Lex r s) { fst := a, snd := b }
Equations
source
def PSigma.lex {α : Sort u} {β : α → Sort v} (ha : WellFoundedRelation α) (hb : (a : α) → WellFoundedRelation (β a)) :
WellFoundedRelation (PSigma β)
Equations
  • One or more equations did not get rendered due to their size.
source
instance PSigma.instWellFoundedRelationPSigma {α : Sort u} {β : α → Sort v} [ha : WellFoundedRelation α] [hb : (a : α) → WellFoundedRelation (β a)] :
WellFoundedRelation (PSigma β)
Equations
  • PSigma.instWellFoundedRelationPSigma = PSigma.lex ha hb
source
def PSigma.lexNdep {α : Sort u} {β : Sort v} (r : α → α → Prop) (s : β → β → Prop) :
(_ : α) ×' β → (_ : α) ×' β → Prop
Equations
source
def PSigma.lexNdepWf {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) :
WellFounded (PSigma.lexNdep r s)
Equations
source
inductive PSigma.RevLex {α : Sort u} {β : Sort v} (r : α → α → Prop) (s : β → β → Prop) :
(_ : α) ×' β → (_ : α) ×' β → Prop
  • left: ∀ {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} {a₁ a₂ : α} (b : β), r a₁ a₂ → PSigma.RevLex r s { fst := a₁, snd := b } { fst := a₂, snd := b }
  • right: ∀ {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (a₁ : α) {b₁ : β} (a₂ : α) {b₂ : β}, s b₁ b₂ → PSigma.RevLex r s { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ }
source
def PSigma.revLexAccessible {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} {b : β} (acb : Acc s b) (aca : ∀ (a : α), Acc r a) (a : α) :
Acc (PSigma.RevLex r s) { fst := a, snd := b }
Equations
source
def PSigma.revLex {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) :
WellFounded (PSigma.RevLex r s)
Equations
source
def PSigma.SkipLeft (α : Type u) {β : Type v} (s : β → β → Prop) :
(_ : α) ×' β → (_ : α) ×' β → Prop
Equations
source
def PSigma.skipLeft (α : Type u) {β : Type v} (hb : WellFoundedRelation β) :
WellFoundedRelation ((_ : α) ×' β)
Equations
source
def PSigma.mkSkipLeft {α : Type u} {β : Type v} {b₁ : β} {b₂ : β} {s : β → β → Prop} (a₁ : α) (a₂ : α) (h : s b₁ b₂) :
PSigma.SkipLeft α s { fst := a₁, snd := b₁ } { fst := a₂, snd := b₂ }
Equations