Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: inequalities of decreasing lists #7896

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - feat: inequalities of decreasing lists #7896

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
290df70
feat: inequalities of decreasing lists
dagurtomas Oct 24, 2023
4e697ef
Update Chain.lean
dagurtomas Oct 24, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 25 additions & 0 deletions Mathlib/Data/List/Chain.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -441,6 +441,31 @@ theorem relationReflTransGen_of_exists_chain (l : List α) (hl₁ : Chain r a l)
Relation.ReflTransGen.refl
#align list.relation_refl_trans_gen_of_exists_chain List.relationReflTransGen_of_exists_chain

theorem Chain'.cons_of_le [LinearOrder α] {a : α} {as m : List α}
(ha : List.Chain' (· > ·) (a :: as)) (hm : List.Chain' (· > ·) m) (hmas : m ≤ as) :
List.Chain' (· > ·) (a :: m) := by
cases m with
| nil => simp only [List.chain'_singleton]
| cons b bs =>
apply hm.cons
cases as with
| nil =>
simp only [le_iff_lt_or_eq, or_false] at hmas
exact (List.Lex.not_nil_right (·<·) _ hmas).elim
| cons a' as =>
rw [List.chain'_cons] at ha
refine gt_of_gt_of_ge ha.1 ?_
rw [le_iff_lt_or_eq] at hmas
cases' hmas with hmas hmas
· by_contra' hh
rw [← not_le] at hmas
apply hmas
apply le_of_lt
exact (List.lt_iff_lex_lt _ _).mp (List.lt.head _ _ hh)
· simp only [List.cons.injEq] at hmas
rw [ge_iff_le, le_iff_lt_or_eq]
exact Or.inr hmas.1

end List


Expand Down
Loading