mathlib documentation

core.init.data.sigma.lex

inductive psigma.lex {α : Sort u} {β : α → Sort v} :
(α → α → Prop)(Π (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 a₁, b₁⟩ a₂, 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 a, b₁⟩ a, b₂⟩

def psigma.lex_accessible {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : Π (a : α), β aβ a → Prop} {a : α} (aca : acc r a) (acb : ∀ (a : α), well_founded (s a)) (b : β a) :
acc (psigma.lex r s) a, b⟩

def psigma.lex_wf {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : Π (a : α), β aβ a → Prop} :
well_founded r(∀ (x : α), well_founded (s x))well_founded (psigma.lex r s)

def psigma.lex_ndep {α : Sort u} {β : Sort v} :
(α → α → Prop)(β → β → Prop)(Σ' (a : α), β)(Σ' (a : α), β) → Prop

Equations
def psigma.lex_ndep_wf {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} :

inductive psigma.rev_lex {α : Sort u} {β : Sort v} :
(α → α → Prop)(β → β → Prop)(Σ' (a : α), β)(Σ' (a : α), β) → Prop
  • left : ∀ {α : Sort u} {β : Sort v} (r : α → α → Prop) (s : β → β → Prop) {a₁ a₂ : α} (b : β), r a₁ a₂psigma.rev_lex r s a₁, b⟩ a₂, b⟩
  • right : ∀ {α : Sort u} {β : Sort v} (r : α → α → Prop) (s : β → β → Prop) (a₁ : α) {b₁ : β} (a₂ : α) {b₂ : β}, s b₁ b₂psigma.rev_lex r s a₁, b₁⟩ a₂, b₂⟩

def psigma.rev_lex_accessible {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} {b : β} (acb : acc s b) (aca : ∀ (a : α), acc r a) (a : α) :
acc (psigma.rev_lex r s) a, b⟩

def psigma.rev_lex_wf {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} :

def psigma.skip_left (α : Type u) {β : Type v} :
(β → β → Prop)(Σ' (a : α), β)(Σ' (a : α), β) → Prop

Equations
def psigma.skip_left_wf (α : Type u) {β : Type v} {s : β → β → Prop} :

def psigma.mk_skip_left {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → Prop} (a₁ a₂ : α) :
s b₁ b₂psigma.skip_left α s a₁, b₁⟩ a₂, b₂⟩

@[instance]
def psigma.has_well_founded {α : Type u} {β : α → Type v} [s₁ : has_well_founded α] [s₂ : Π (a : α), has_well_founded (β a)] :

Equations