feat(library/data/nat/wf): define measure using inverse image
This commit is contained in:
parent
4623a62ec3
commit
76711d00c1
1 changed files with 6 additions and 0 deletions
|
@ -43,4 +43,10 @@ well_founded.intro
|
||||||
(assume Hlt : m < n, acc.inv iH Hlt)
|
(assume Hlt : m < n, acc.inv iH Hlt)
|
||||||
(assume Heq : m = n, Heq⁻¹ ▸ iH))))
|
(assume Heq : m = n, Heq⁻¹ ▸ iH))))
|
||||||
|
|
||||||
|
definition measure {A : Type} (f : A → nat) : A → A → Prop :=
|
||||||
|
inv_image lt f
|
||||||
|
|
||||||
|
definition measure.wf {A : Type} (f : A → nat) : well_founded (measure f) :=
|
||||||
|
inv_image.wf f lt.wf
|
||||||
|
|
||||||
end nat
|
end nat
|
||||||
|
|
Loading…
Reference in a new issue