mathlib documentation

core / init.data.sigma.lex

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 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₂⟩
theorem 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⟩
theorem psigma.lex_wf {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : Π (a : α), β aβ a → Prop} (ha : well_founded r) (hb : ∀ (x : α), well_founded (s x)) :
def psigma.lex_ndep {α : Sort u} {β : Sort v} (r : α → α → Prop) (s : β → β → Prop) :
(Σ' (a : α), β)(Σ' (a : α), β) → Prop
Equations
theorem psigma.lex_ndep_wf {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (ha : well_founded r) (hb : well_founded s) :
inductive psigma.rev_lex {α : Sort u} {β : Sort v} (r : α → α → Prop) (s : β → β → 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₂⟩
theorem 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⟩
theorem psigma.rev_lex_wf {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (ha : well_founded r) (hb : well_founded s) :
def psigma.skip_left (α : Type u) {β : Type v} (s : β → β → Prop) :
(Σ' (a : α), β)(Σ' (a : α), β) → Prop
Equations
theorem psigma.skip_left_wf (α : Type u) {β : Type v} {s : β → β → Prop} (hb : well_founded s) :
theorem psigma.mk_skip_left {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → Prop} (a₁ a₂ : α) (h : s b₁ b₂) :
psigma.skip_left α s a₁, b₁⟩ a₂, b₂⟩
@[protected, instance]
def psigma.has_well_founded {α : Type u} {β : α → Type v} [s₁ : has_well_founded α] [s₂ : Π (a : α), has_well_founded (β a)] :
Equations