max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/sigma_lex): add lex_ndep for sigma types

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-09 08:54:13 -07:00
parent 75904f6dc6
commit 8d2a3fc980
1 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
library/init/sigma_lex.lean
View file

@ -51,6 +51,16 @@ section
-- The lexicographical order of well founded relations is well-founded
definition lex_wf (Ha : well_founded Ra) (Hb : ∀ x, well_founded (Rb x)) : well_founded (lex Ra Rb) :=
well_founded.intro (λp, destruct p (λa b, lex_accessible (well_founded.apply Ha a) Hb b))
end
section
parameters {A : Type} {B : Type}
definition lex_ndep (Ra : A → A → Prop) (Rb : B → B → Prop) :=
lex Ra (λ a : A, Rb)
definition lex_ndep_wf {Ra : A → A → Prop} {Rb : B → B → Prop} (Ha : well_founded Ra) (Hb : well_founded Rb)
: well_founded (lex_ndep Ra Rb) :=
well_founded.intro (λp, destruct p (λa b, lex_accessible (well_founded.apply Ha a) (λ x, Hb) b))
end
end sigma