- 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⟩
Equations
- _ = _
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
- psigma.lex_ndep r s = psigma.lex r (λ (a : α), s)
def
psigma.lex_ndep_wf
{α : Sort u}
{β : Sort v}
{r : α → α → Prop}
{s : β → β → Prop} :
well_founded r → well_founded s → well_founded (psigma.lex_ndep r s)
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⟩
Equations
- _ = _
def
psigma.rev_lex_wf
{α : Sort u}
{β : Sort v}
{r : α → α → Prop}
{s : β → β → Prop} :
well_founded r → well_founded s → well_founded (psigma.rev_lex r s)
def
psigma.skip_left
(α : Type u)
{β : Type v} :
(β → β → Prop) → (Σ' (a : α), β) → (Σ' (a : α), β) → Prop
Equations
def
psigma.skip_left_wf
(α : Type u)
{β : Type v}
{s : β → β → Prop} :
well_founded s → well_founded (psigma.skip_left α s)
Equations
- _ = _
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₂⟩
Equations
- _ = _
@[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 := _}