inductive
psigma.lex
{α : Sort u}
{β : α → Sort v}
(r : α → α → Prop)
(s : Π (a : α), β a → β a → 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)) :
well_founded (psigma.lex r s)
def
psigma.lex_ndep
{α : Sort u}
{β : Sort v}
(r : α → α → Prop)
(s : β → β → Prop) :
(Σ' (a : α), β) → (Σ' (a : α), β) → Prop
Equations
- psigma.lex_ndep r s = psigma.lex r (λ (a : α), s)
theorem
psigma.lex_ndep_wf
{α : Sort u}
{β : Sort v}
{r : α → α → Prop}
{s : β → β → Prop}
(ha : well_founded r)
(hb : well_founded s) :
well_founded (psigma.lex_ndep r 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) :
well_founded (psigma.rev_lex r 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) :
well_founded (psigma.skip_left α 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
- psigma.has_well_founded = {r := psigma.lex has_well_founded.r (λ (a : α), has_well_founded.r), wf := _}