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

feat: generalize IsLUB.mem_of_not_isSuccPrelimit to LinearOrder #20502

Open
wants to merge 7 commits into
base: master
Choose a base branch
from
+41 −14
Open

feat: generalize IsLUB.mem_of_not_isSuccPrelimit to LinearOrder #20502

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
cef1b6c
generalize
vihdzp Jan 6, 2025
3c69b33
add other aux lemma
vihdzp Jan 6, 2025
1db7883
fix
vihdzp Jan 6, 2025
c2fe20c
Merge branch 'master' into vi.limitLemmas
vihdzp Jan 13, 2025
a6da152
apply suggestions
vihdzp Jan 19, 2025
64a2422
Merge branch 'master' into vi.limitLemmas
vihdzp Jan 19, 2025
b6f79ad
fix
vihdzp Jan 19, 2025
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
16 changes: 2 additions & 14 deletions Mathlib/Order/SuccPred/CompleteLinearOrder.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -124,14 +124,7 @@ lemma exists_eq_ciSup_of_not_isSuccPrelimit'
@[deprecated exists_eq_ciSup_of_not_isSuccPrelimit' (since := "2024-09-05")]
alias exists_eq_ciSup_of_not_isSuccLimit' := exists_eq_ciSup_of_not_isSuccPrelimit'

lemma IsLUB.mem_of_not_isSuccPrelimit (hs : IsLUB s x) (hx : ¬ IsSuccPrelimit x) : x ∈ s := by
obtain rfl | hs' := s.eq_empty_or_nonempty
· simp [show x = ⊥ by simpa using hs, isSuccPrelimit_bot] at hx
· exact hs.mem_of_nonempty_of_not_isSuccPrelimit hs' hx

@[deprecated IsLUB.mem_of_not_isSuccPrelimit (since := "2024-09-05")]
alias IsLUB.mem_of_not_isSuccLimit := IsLUB.mem_of_not_isSuccPrelimit

@[deprecated IsLUB.mem_of_not_isSuccPrelimit (since := "2025-01-05")]
lemma IsLUB.exists_of_not_isSuccPrelimit (hf : IsLUB (range f) x) (hx : ¬ IsSuccPrelimit x) :
∃ i, f i = x :=
hf.mem_of_not_isSuccPrelimit hx
Expand Down Expand Up @@ -206,12 +199,7 @@ lemma exists_eq_iInf_of_not_isPredPrelimit (hf : ¬ IsPredPrelimit (⨅ i, f i))
@[deprecated exists_eq_iInf_of_not_isPredPrelimit (since := "2024-09-05")]
alias exists_eq_iInf_of_not_isPredLimit := exists_eq_iInf_of_not_isPredPrelimit

lemma IsGLB.mem_of_not_isPredPrelimit (hs : IsGLB s x) (hx : ¬ IsPredPrelimit x) : x ∈ s :=
hs.sInf_eq ▸ sInf_mem_of_not_isPredPrelimit (hs.sInf_eq ▸ hx)

@[deprecated IsGLB.mem_of_not_isPredPrelimit (since := "2024-09-05")]
alias IsGLB.mem_of_not_isPredLimit := IsGLB.mem_of_not_isPredPrelimit

@[deprecated IsGLB.mem_of_not_isPredLimit (since := "2025-01-05")]
lemma IsGLB.exists_of_not_isPredPrelimit (hf : IsGLB (range f) x) (hx : ¬ IsPredPrelimit x) :
∃ i, f i = x :=
hf.mem_of_not_isPredPrelimit hx
Expand Down
39 changes: 39 additions & 0 deletions Mathlib/Order/SuccPred/Limit.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -324,6 +324,29 @@ theorem IsSuccPrelimit.lt_iff_exists_lt (h : IsSuccPrelimit b) : a < b ↔ ∃ c
theorem IsSuccLimit.lt_iff_exists_lt (h : IsSuccLimit b) : a < b ↔ ∃ c < b, a < c :=
h.isSuccPrelimit.lt_iff_exists_lt

lemma _root_.IsLUB.isSuccPrelimit_of_not_mem {s : Set α} (hs : IsLUB s a) (ha : a ∉ s) :
IsSuccPrelimit a := by
intro b hb
obtain ⟨c, hc, hbc, hca⟩ := hs.exists_between hb.lt
obtain rfl := (hb.ge_of_gt hbc).antisymm hca
contradiction

lemma _root_.IsLUB.mem_of_not_isSuccPrelimit {s : Set α} (hs : IsLUB s a) (ha : ¬IsSuccPrelimit a) :
a ∈ s :=
ha.imp_symm hs.isSuccPrelimit_of_not_mem

lemma _root_.IsLUB.isSuccLimit_of_not_mem {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty)
(ha : a ∉ s) : IsSuccLimit a := by
refine ⟨?_, hs.isSuccPrelimit_of_not_mem ha⟩
obtain ⟨b, hb⟩ := hs'
obtain rfl | hb := (hs.1 hb).eq_or_lt
· contradiction
· exact hb.not_isMin

lemma _root_.IsLUB.mem_of_not_isSuccLimit {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty)
(ha : ¬IsSuccLimit a) : a ∈ s :=
ha.imp_symm <| hs.isSuccLimit_of_not_mem hs'

theorem IsSuccPrelimit.isLUB_Iio (ha : IsSuccPrelimit a) : IsLUB (Iio a) a := by
refine ⟨fun _ ↦ le_of_lt, fun b hb ↦ le_of_forall_lt fun c hc ↦ ?_⟩
obtain ⟨d, hd, hd'⟩ := ha.lt_iff_exists_lt.1 hc
Expand Down Expand Up @@ -634,6 +657,22 @@ theorem IsPredPrelimit.lt_iff_exists_lt (h : IsPredPrelimit b) : b < a ↔ ∃ c
theorem IsPredLimit.lt_iff_exists_lt (h : IsPredLimit b) : b < a ↔ ∃ c, b < c ∧ c < a :=
h.dual.lt_iff_exists_lt

lemma _root_.IsGLB.isPredPrelimit_of_not_mem {s : Set α} (hs : IsGLB s a) (ha : a ∉ s) :
IsPredPrelimit a := by
simpa using (IsGLB.dual hs).isSuccPrelimit_of_not_mem ha

lemma _root_.IsGLB.mem_of_not_isPredPrelimit {s : Set α} (hs : IsGLB s a) (ha : ¬IsPredPrelimit a) :
a ∈ s :=
ha.imp_symm hs.isPredPrelimit_of_not_mem

lemma _root_.IsGLB.isPredLimit_of_not_mem {s : Set α} (hs : IsGLB s a) (hs' : s.Nonempty)
(ha : a ∉ s) : IsPredLimit a := by
simpa using (IsGLB.dual hs).isSuccLimit_of_not_mem hs' ha

lemma _root_.IsGLB.mem_of_not_isPredLimit {s : Set α} (hs : IsGLB s a) (hs' : s.Nonempty)
(ha : ¬IsPredLimit a) : a ∈ s :=
ha.imp_symm <| hs.isPredLimit_of_not_mem hs'

theorem IsPredPrelimit.isGLB_Ioi (ha : IsPredPrelimit a) : IsGLB (Ioi a) a :=
ha.dual.isLUB_Iio

Expand Down
Loading