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.

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: lemmas about intervals and finite intervals #22199

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
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
31 changes: 31 additions & 0 deletions Mathlib/Order/Interval/Finset/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -402,6 +402,9 @@ theorem Ico_subset_Iic_self : Ico a b ⊆ Iic b :=
theorem Ioo_subset_Iic_self : Ioo a b ⊆ Iic b :=
Ioo_subset_Ioc_self.trans Ioc_subset_Iic_self

theorem Iic_disjoint_Ioc (h : a ≤ b) : Disjoint (Iic a) (Ioc b c) :=
disjoint_left.2 fun _ hax hbcx ↦ (mem_Iic.1 hax).not_lt <| lt_of_le_of_lt h (mem_Ioc.1 hbcx).1

end LocallyFiniteOrderBot

section LocallyFiniteOrderTop
Expand Down Expand Up @@ -721,6 +724,15 @@ lemma sup'_Iic (a : α) : (Iic a).sup' nonempty_Iic id = a :=
@[simp] lemma sup_Iic [OrderBot α] (a : α) : (Iic a).sup id = a :=
le_antisymm (Finset.sup_le fun _ ↦ mem_Iic.1) <| le_sup (f := id) <| mem_Iic.2 <| le_refl a

lemma subset_Iic_sup [OrderBot α] [DecidableEq α] (f : ι → α) (s : Finset ι) :
s.image f ⊆ (Iic (s.sup f)) := by
refine fun i hi ↦ mem_Iic.2 ?_
obtain ⟨j, hj, rfl⟩ := mem_image.1 hi
exact le_sup hj

lemma subset_Iic_sup_id [OrderBot α] (s : Finset α) : s ⊆ (Iic (s.sup id)) :=
fun _ h ↦ mem_Iic.2 <| le_sup (f := id) h

end SemilatticeSup

section SemilatticeInf
Expand Down Expand Up @@ -811,6 +823,25 @@ theorem Ico_diff_Ico_right (a b c : α) : Ico a b \ Ico c b = Ico a (min b c) :=
rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, min_eq_right h, and_assoc, not_and', not_le]
exact and_congr_right' ⟨fun hx => hx.2 hx.1, fun hx => ⟨hx.trans_le h, fun _ => hx⟩⟩

section LocallyFiniteOrderBot

variable [LocallyFiniteOrderBot α]

theorem Iic_diff_Ioc : Iic b \ Ioc a b = Iic (a ⊓ b) := by
rw [← coe_inj]
push_cast
exact Set.Iic_diff_Ioc

theorem Iic_diff_Ioc_self_of_le (hab : a ≤ b) : Iic b \ Ioc a b = Iic a := by
rw [Iic_diff_Ioc, min_eq_left hab]

theorem Iic_union_Ioc_eq_Iic (h : a ≤ b) : Iic a ∪ Ioc a b = Iic b := by
rw [← coe_inj]
push_cast
exact Set.Iic_union_Ioc_eq_Iic h

end LocallyFiniteOrderBot

end LocallyFiniteOrder

section LocallyFiniteOrderBot
Expand Down
6 changes: 6 additions & 0 deletions Mathlib/Order/Interval/Finset/Nat.lean
Original file line number Diff line number Diff line change
Expand Up @@ -134,6 +134,12 @@ theorem Ioc_succ_singleton : Ioc b (b + 1) = {b + 1} := by rw [← Nat.Icc_succ_

variable {a b c}

lemma mem_Ioc_succ (h : a ∈ Ioc b (b + 1)) : a = b + 1 :=
eq_of_mem_singleton (Ioc_succ_singleton b ▸ h)

lemma mem_Ioc_succ' (a : Ioc b (b + 1)) : a = ⟨b + 1, mem_Ioc.2 (by omega)⟩ :=
Subtype.val_inj.1 (mem_Ioc_succ a.2)

theorem Ico_succ_right_eq_insert_Ico (h : a ≤ b) : Ico a (b + 1) = insert b (Ico a b) := by
rw [Ico_succ_right, ← Ico_insert_right h]

Expand Down
11 changes: 11 additions & 0 deletions Mathlib/Order/Interval/Set/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1490,6 +1490,17 @@ theorem Ico_inter_Iio : Ico a b ∩ Iio c = Ico a (min b c) :=
theorem Ioc_diff_Iic : Ioc a b \ Iic c = Ioc (max a c) b := by
rw [diff_eq, compl_Iic, Ioc_inter_Ioi]

theorem compl_Ioc : (Ioc a b)ᶜ = Iic a ∪ Ioi b := by
ext i
rw [mem_compl_iff, mem_Ioc, mem_union, mem_Iic, mem_Ioi, not_and_or, not_lt, not_le]

theorem Iic_diff_Ioc : Iic b \ Ioc a b = Iic (a ⊓ b) := by
rw [diff_eq, compl_Ioc, inter_union_distrib_left, Iic_inter_Iic, ← compl_Iic, inter_compl_self,
union_empty, min_comm]

theorem Iic_diff_Ioc_self_of_le (hab : a ≤ b) : Iic b \ Ioc a b = Iic a := by
rw [Iic_diff_Ioc, min_eq_left hab]

@[simp]
theorem Ioc_union_Ioc_right : Ioc a b ∪ Ioc a c = Ioc a (max b c) := by
rw [Ioc_union_Ioc, min_self] <;> exact (min_le_left _ _).trans (le_max_left _ _)
Expand Down