Skip to content

Commit

Permalink
refactor(lebesgue_measure): clean up proofs
Browse files Browse the repository at this point in the history
  • Loading branch information
@digama0
digama0 committed Apr 19, 2018
1 parent 7d1ab38 commit 2d935cb
Show file tree
Hide file tree
Showing 9 changed files with 81 additions and 135 deletions.
17 changes: 3 additions & 14 deletions algebra/ordered_group.lean
View file
Expand Up @@ -245,20 +245,6 @@ lemma sub_lt_sub_iff_left (a : α) {b c : α} : a - b < a - c ↔ c < b :=
lemma sub_lt_sub_iff_right (c : α) : a - c < b - c ↔ a < b :=
add_lt_add_iff_right _

lemma sub_lt_iff {a b c : α} : (a - b < c) ↔ (a < c + b) :=
iff.intro
lt_add_of_sub_right_lt
(assume h,
have a + - b < (c + b) + - b, from add_lt_add_right h _,
by simp * at *)

lemma lt_sub_iff {a b c : α} : (a < b - c) ↔ (a + c < b) :=
iff.intro
(assume h,
have a + c < (b - c) + c, from add_lt_add_right h _,
by simp * at *)
lt_sub_right_of_add_lt

@[simp] lemma sub_nonneg : 0 ≤ a - b ↔ b ≤ a :=
have a - a ≤ a - b ↔ b ≤ a, from sub_le_sub_iff_left a,
by rwa sub_self at this
Expand Down Expand Up @@ -348,6 +334,9 @@ by rw [neg_lt_sub_iff_lt_add, add_comm]
lemma sub_lt : a - b < c ↔ a - c < b :=
sub_lt_iff_lt_add'.trans sub_lt_iff_lt_add.symm

theorem lt_sub : a < b - c ↔ c < b - a :=
lt_sub_iff_add_lt'.trans lt_sub_iff_add_lt.symm

lemma sub_le_self_iff (a : α) {b : α} : a - b ≤ a ↔ 0 ≤ b :=
sub_le_iff_le_add'.trans (le_add_iff_nonneg_left _)

Expand Down
4 changes: 2 additions & 2 deletions algebra/ordered_ring.lean
View file
Expand Up @@ -76,7 +76,7 @@ instance linear_ordered_semiring.to_no_top_order {α : Type*} [linear_ordered_se

instance linear_ordered_semiring.to_no_bot_order {α : Type*} [linear_ordered_ring α] :
no_bot_order α :=
⟨assume a, ⟨a - 1, sub_lt_iff.mpr $ lt_add_of_pos_right _ zero_lt_one⟩⟩
⟨assume a, ⟨a - 1, sub_lt_iff_lt_add.mpr $ lt_add_of_pos_right _ zero_lt_one⟩⟩

instance to_domain [s : linear_ordered_ring α] : domain α :=
{ eq_zero_or_eq_zero_of_mul_eq_zero := @linear_ordered_ring.eq_zero_or_eq_zero_of_mul_eq_zero α s,
Expand All @@ -100,7 +100,7 @@ le_iff_le_iff_lt_iff_lt.1 (mul_le_mul_left_of_neg h)
le_iff_le_iff_lt_iff_lt.1 (mul_le_mul_right_of_neg h)

lemma sub_one_lt (a : α) : a - 1 < a :=
sub_lt_iff.2 (lt_add_one a)
sub_lt_iff_lt_add.2 (lt_add_one a)

end linear_ordered_ring

Expand Down
12 changes: 6 additions & 6 deletions analysis/ennreal.lean
View file
Expand Up @@ -394,7 +394,7 @@ suffices ∀r, 0 ≤ r → of_real r > b → a ≤ of_real r,
assume r hr hrb,
let ⟨p, hp, b_eq, hpr⟩ := lt_iff_exists_of_real.mp hrb in
have p < r, by simp [hp, hr] at hpr; assumption,
have pos : 0 < r - p, from lt_sub_iff.mpr $ by simp [this],
have pos : 0 < r - p, from lt_sub_iff_add_lt.mpr $ by simp [this],
calc a ≤ b + of_real (r - p) : h _ pos (by simp [b_eq])
... = of_real r :
by simp [-sub_eq_add_neg, le_of_lt pos, hp, hr, b_eq]; simp [sub_eq_add_neg]
Expand Down Expand Up @@ -493,8 +493,8 @@ instance : complete_linear_order ennreal :=
Inf_le := assume s a ha, ennreal.Sup_le $ assume b hb, hb _ ha,
..ennreal.decidable_linear_order }

protected lemma bot_eq_zero : (⊥ : ennreal) = 0 := rfl
protected lemma top_eq_infty : (⊤ : ennreal) = ∞ := rfl
@[simp] protected lemma bot_eq_zero : (⊥ : ennreal) = 0 := rfl
@[simp] protected lemma top_eq_infty : (⊤ : ennreal) = ∞ := rfl

end complete_lattice

Expand Down Expand Up @@ -630,8 +630,8 @@ begin
apply tendsto_principal.2 _,
revert b,
simp [forall_ennreal],
exact assume r hr hr', mem_prod_iff.mpr ⟨
{a | of_real r < a}, mem_nhds_sets (is_open_lt' _) hr',
exact assume r hr, mem_prod_iff.mpr ⟨
{a | of_real r < a}, mem_nhds_sets (is_open_lt' _) of_real_lt_infty,
univ, univ_mem_sets, assume ⟨c, d⟩ ⟨hc, _⟩, lt_of_lt_of_le hc $ le_add_right $ le_refl _⟩
end,
have h : ∀{p r : ℝ}, 0 ≤ p → 0 ≤ r → tendsto (λp:ennreal×ennreal, p.1 + p.2)
Expand Down Expand Up @@ -992,7 +992,7 @@ le_antisymm
finset.sum_le_sum_of_ne_zero $ assume b _ hb,
suffices a = b, by simpa using this.symm,
classical.by_contradiction $ assume h,
by simp [h] at hb; exact hb rfl
by simpa [h] using hb
... = f a : by simp))
(calc f a ≤ (⨆ (h : a = a), f a) : le_supr (λh:a=a, f a) rfl
... ≤ (∑b:α, ⨆ (h : a = b), f b) : ennreal.le_tsum)
Expand Down
2 changes: 1 addition & 1 deletion analysis/limits.lean
View file
Expand Up @@ -82,7 +82,7 @@ lemma tendsto_pow_at_top_at_top_of_gt_1 {r : ℝ} (h : r > 1) : tendsto (λn:ℕ
tendsto_infi.2 $ assume p, tendsto_principal.2 $
let ⟨n, hn⟩ := exists_nat_gt (p / (r - 1)) in
have hn_nn : (0:ℝ) ≤ n, from nat.cast_nonneg n,
have r - 1 > 0, from sub_lt_iff.mp $ by simp; assumption,
have r - 1 > 0, from sub_lt_iff_lt_add.mp $ by simp; assumption,
have p ≤ r ^ n,
from calc p = (p / (r - 1)) * (r - 1) : (div_mul_cancel _ $ ne_of_gt this).symm
... ≤ n * (r - 1) : mul_le_mul (le_of_lt hn) (le_refl _) (le_of_lt this) hn_nn
Expand Down
145 changes: 36 additions & 109 deletions analysis/measure_theory/lebesgue_measure.lean
View file
Expand Up @@ -18,7 +18,7 @@ Important: if `s` is not a interval [a, b) its value is `∞`. This is important
Lebesgue measure. -/
def lebesgue_length (s : set ℝ) : ennreal := ⨅a b (h₁ : a ≤ b) (h₂ : s = Ico a b), of_real (b - a)

@[simp] lemma lebesgue_length_Ico {a b : ℝ} (h : a ≤ b) :
lemma lebesgue_length_Ico' {a b : ℝ} (h : a ≤ b) :
lebesgue_length (Ico a b) = of_real (b - a) :=
le_antisymm
(infi_le_of_le a $ infi_le_of_le b $ infi_le_of_le h $ infi_le_of_le rfl $ le_refl _)
Expand All @@ -32,25 +32,22 @@ le_antisymm
end)

@[simp] lemma lebesgue_length_empty : lebesgue_length ∅ = 0 :=
have ∅ = Ico 0 (0:ℝ),
from set.ext $ by simp [Ico, not_le],
by rw [this, lebesgue_length_Ico]; simp [le_refl]
by rw [← (Ico_self : Ico 0 (0:ℝ) = ∅), lebesgue_length_Ico'];
simp [le_refl]

lemma le_lebesgue_length {r : ennreal} {s : set ℝ } (h : ∀a b, a ≤ b → s ≠ Ico a b) :
@[simp] lemma lebesgue_length_Ico {a b : ℝ} :
lebesgue_length (Ico a b) = of_real (b - a) :=
(le_total a b).elim lebesgue_length_Ico' $ λ h,
by rw [ennreal.of_real_of_nonpos (sub_nonpos.2 h), Ico_eq_empty h]; simp

lemma le_lebesgue_length {r : ennreal} {s : set ℝ} (h : ∀a b, a ≤ b → s ≠ Ico a b) :
r ≤ lebesgue_length s :=
le_infi $ assume a, le_infi $ assume b, le_infi $ assume hab, le_infi $ assume heq, (h a b hab heq).elim

lemma lebesgue_length_Ico_le_lebesgue_length_Ico {a₁ b₁ a₂ b₂ : ℝ} (ha : a₂ ≤ a₁) (hb : b₁ ≤ b₂) :
lebesgue_length (Ico a₁ b₁) ≤ lebesgue_length (Ico a₂ b₂) :=
(le_total b₁ a₁).elim
(assume : b₁ ≤ a₁, by simp [Ico_eq_empty_iff.mpr this])
(assume h₁ : a₁ ≤ b₁,
have h₂ : a₂ ≤ b₂, from le_trans (le_trans ha h₁) hb,
by simp [h₁, h₂, -sub_eq_add_neg]; exact sub_le_sub hb ha)

lemma lebesgue_length_subadditive {a b : ℝ} {c d : ℕ → ℝ}
(hab : a ≤ b) (hcd : ∀i, c i ≤ d i) (habcd : Ico a b ⊆ (⋃i, Ico (c i) (d i))) :
(hcd : ∀i, c i ≤ d i) (habcd : Ico a b ⊆ (⋃i, Ico (c i) (d i))) :
lebesgue_length (Ico a b) ≤ (∑i, lebesgue_length (Ico (c i) (d i))) :=
(le_total b a).elim (λ h, by rw [Ico_eq_empty h]; simp) $ λ hab,
let
s := λx, ∑i, lebesgue_length (Ico (c i) (min (d i) x)),
M := {x : ℝ | a ≤ x ∧ x ≤ b ∧ of_real (x - a) ≤ s x }
Expand All @@ -72,8 +69,8 @@ have hxb : x ≤ b, from hx.right b ‹b ∈ upper_bounds M›,
have hx_sx : of_real (x - a) ≤ s x,
from h'.right _ $ assume r ⟨y, hy, eq⟩,
have ∀i, lebesgue_length (Ico (c i) (min (d i) y)) ≤ lebesgue_length (Ico (c i) (min (d i) x)),
from assume i,
lebesgue_length_Ico_le_lebesgue_length_Ico (le_refl _) (inf_le_inf (le_refl _) (hx.left _ hy)),
from assume i, by simp; exact
ennreal.of_real_le_of_real (add_le_add_right (inf_le_inf (le_refl _) (hx.left _ hy)) _),
eq ▸ le_trans hy.2.2 $ ennreal.tsum_le_tsum this,
have hxM : x ∈ M,
from ⟨hax, hxb, hx_sx⟩,
Expand Down Expand Up @@ -101,37 +98,32 @@ have x = b,
have h : c k ≤ y, from le_min (hcd _) (le_trans hxc $ le_of_lt hxb),
have eq: y - x + (x - c k) = y - c k, by rw [add_sub, sub_add_cancel],
by simp [h, hxy, hxc, eq, eq₁, eq₂, this, -sub_eq_add_neg, add_sub_cancel'_right, le_refl])
(assume h : i ≠ k, by simp [h, ennreal.bot_eq_zero];
from lebesgue_length_Ico_le_lebesgue_length_Ico (le_refl _) (inf_le_inf (le_refl _) hxy)),
(assume h : i ≠ k, by simp [h];
from ennreal.of_real_le_of_real (add_le_add_right (inf_le_inf (le_refl _) hxy) _)),
have ¬ x < y, from not_lt.mpr $ hx.left y ⟨le_trans hax hxy, min_le_right _ _, this⟩,
this hxy',
have hbM : b ∈ M, from this ▸ hxM,
calc lebesgue_length (Ico a b) ≤ s b : by simp [hab]; exact hbM.right.right
... ≤ ∑i, lebesgue_length (Ico (c i) (d i)) : ennreal.tsum_le_tsum $ assume a,
lebesgue_length_Ico_le_lebesgue_length_Ico (le_refl _) (min_le_left _ _)
by simp; exact ennreal.of_real_le_of_real (add_le_add_right (min_le_left _ _) _)

/-- The Lebesgue outer measure, as an outer measure of ℝ. -/
def lebesgue_outer : outer_measure ℝ :=
outer_measure.of_function lebesgue_length lebesgue_length_empty

lemma lebesgue_outer_Ico {a b : ℝ} (h : a ≤ b) :
lemma lebesgue_outer_Ico {a b : ℝ} :
lebesgue_outer.measure_of (Ico a b) = of_real (b - a) :=
le_antisymm
(let f : ℕ → set ℝ := λi, nat.rec_on i (Ico a b) (λn s, ∅) in
infi_le_of_le f $ infi_le_of_le (subset_Union f 0) $
calc (∑i, lebesgue_length (f i)) = ({0} : finset ℕ).sum (λi, lebesgue_length (f i)) :
tsum_eq_sum $ by intro i; cases i; simp
... = lebesgue_length (Ico a b) : by simp; refl
... ≤ of_real (b - a) : by simp [h])
(by rw ← lebesgue_length_Ico; apply outer_measure.of_function_le)
(le_infi $ assume f, le_infi $ assume hf, by_cases
(assume : ∀i, ∃p:ℝ×ℝ, p.1 ≤ p.2 ∧ f i = Ico p.1 p.2,
let ⟨cd, hcd⟩ := axiom_of_choice this in
have hcd₁ : ∀i, (cd i).1 ≤ (cd i).2, from assume i, (hcd i).1,
have hcd₂ : ∀i, f i = Ico (cd i).1 (cd i).2, from assume i, (hcd i).2,
calc of_real (b - a) = lebesgue_length (Ico a b) :
by simp [h]
by simp
... ≤ (∑i, lebesgue_length (Ico (cd i).1 (cd i).2)) :
lebesgue_length_subadditive h hcd₁ (by simpa [hcd₂] using hf)
lebesgue_length_subadditive hcd₁ (by simpa [hcd₂] using hf)
... = _ :
by simp [hcd₂])
(assume h,
Expand Down Expand Up @@ -174,91 +166,26 @@ tendsto_infi.2 $ assume r, tendsto_principal.2 $
let ⟨n, hn⟩ := exists_nat_gt r in
mem_at_top_sets.2 ⟨n, λ m h, le_trans (le_of_lt hn) (nat.cast_le.2 h)⟩

lemma lebesgue_Ico {a b : ℝ} : lebesgue (Ico a b) = of_real (b - a) :=
match le_total a b with
| or.inl h :=
begin
rw [lebesgue.measure_eq is_measurable_Ico],
{ exact lebesgue_outer_Ico h },
repeat {apply_instance}
end
| or.inr h :=
have hba : b - a ≤ 0, by simp [-sub_eq_add_neg, h],
have eq : Ico a b = ∅, from Ico_eq_empty_iff.mpr h,
by simp [ennreal.of_real_of_nonpos, *] at *
end
@[simp] lemma lebesgue_Ico {a b : ℝ} : lebesgue (Ico a b) = of_real (b - a) :=
by rw [lebesgue.measure_eq is_measurable_Ico]; exact lebesgue_outer_Ico

lemma lebesgue_Ioo {a b : ℝ} : lebesgue (Ioo a b) = of_real (b - a) :=
by_cases (assume h : b ≤ a, by simp [h, -sub_eq_add_neg, ennreal.of_real_of_nonpos]) $
assume : ¬ b ≤ a,
have h : a < b, from not_le.mp this,
let s := λn:ℕ, a + (b - a) * (↑(n + 1))⁻¹ in
have tendsto s at_top (nhds (a + (b - a) * 0)),
from tendsto_add tendsto_const_nhds $ tendsto_mul tendsto_const_nhds $
(tendsto_comp_succ_at_top_iff.mpr tendsto_of_nat_at_top_at_top).comp tendsto_inverse_at_top_nhds_0,
have hs : tendsto s at_top (nhds a), by simpa,
have hsm : ∀i j, j ≤ i → s i ≤ s j,
from assume i j hij,
have h₁ : ∀j:ℕ, (0:ℝ) < (j + 1),
from assume j, nat.cast_pos.2 $ add_pos_of_nonneg_of_pos (nat.zero_le j) zero_lt_one,
have h₂ : (↑(j + 1) : ℝ) ≤ ↑(i + 1), from nat.cast_le.2 $ add_le_add hij (le_refl _),
add_le_add (le_refl _) $
mul_le_mul (le_refl _) (inv_le_inv_of_le (h₁ j) h₂) (le_of_lt $ inv_pos $ h₁ i) $
by simp [le_sub_iff_add_le, -sub_eq_add_neg, le_of_lt h],
have has : ∀i, a < s i,
from assume i,
have (0:ℝ) < ↑(i + 1), from nat.cast_pos.2 $ lt_add_of_le_of_pos (nat.zero_le _) zero_lt_one,
(lt_add_iff_pos_right _).mpr $ mul_pos
(by simp [-sub_eq_add_neg, sub_lt_iff, (>), ‹a < b›]) (inv_pos this),
have eq₁ : Ioo a b = (⋃n, Ico (s n) b),
from set.ext $ assume x,
begin
simp [iff_def, Ico, Ioo, -sub_eq_add_neg] {contextual := tt},
constructor,
exact assume hax hxb,
have {a | a < x } ∈ (nhds a).sets, from mem_nhds_sets (is_open_gt' _) hax,
have {n | s n < x} ∈ at_top.sets, from hs this,
let ⟨n, hn⟩ := inhabited_of_mem_sets at_top_ne_bot this in
⟨n, le_of_lt hn⟩,
exact assume i hsx hxb, lt_of_lt_of_le (has i) hsx,
end,
have (⨆i, of_real (b - s i)) = of_real (b - a),
from is_lub_iff_supr_eq.mp $ is_lub_of_mem_nhds
(assume x ⟨i, eq⟩, eq ▸ ennreal.of_real_le_of_real $ sub_le_sub (le_refl _) $ le_of_lt $ has _)
begin
show range (λi, of_real (b - s i)) ∈ (at_top.map (λi, of_real (b - s i))).sets,
rw [← image_univ]; exact image_mem_map univ_mem_sets
end
begin
have : tendsto (λi, of_real (b - s i)) at_top (nhds (of_real (b - a))),
from (tendsto_sub tendsto_const_nhds hs).comp ennreal.tendsto_of_real,
rw [inf_of_le_left this],
exact map_ne_bot at_top_ne_bot
end,
have eq₂ : (⨆i, lebesgue (Ico (s i) b)) = of_real (b - a),
by simp only [lebesgue_Ico, this],
@[simp] lemma lebesgue_Ioo {a b : ℝ} : lebesgue (Ioo a b) = of_real (b - a) :=
begin
rw [eq₁, measure_Union_eq_supr_nat, eq₂],
show ∀i, is_measurable (Ico (s i) b), from assume i, is_measurable_Ico,
show monotone (λi, Ico (s i) b),
from assume i j hij x hx, ⟨le_trans (hsm _ _ hij) hx.1, hx.2⟩
cases le_total b a with ba ab,
{ rw ennreal.of_real_of_nonpos (sub_nonpos.2 ba), simp [ba] },
refine (eq_of_le_of_forall_ge_of_dense _ (λ r h, _)).symm,
{ rw ← lebesgue_Ico,
exact measure_mono Ioo_subset_Ico_self },
rcases ennreal.lt_iff_exists_of_real.1 h with ⟨c, c0, rfl, _⟩,
replace h := (ennreal.of_real_lt_of_real_iff c0 (sub_nonneg.2 ab)).1 h,
rw ← show lebesgue (Ico (b - c) b) = of_real c,
by simp [-sub_eq_add_neg, sub_sub_cancel],
exact measure_mono (Ico_subset_Ioo_left $ lt_sub.1 h)
end

lemma lebesgue_singleton {a : ℝ} : lebesgue {a} = 0 :=
have Ico a (a + 1) \ Ioo a (a + 1) = {a},
from set.ext $ assume a',
begin
simp [iff_def, Ico, Ioo, lt_irrefl, le_refl, zero_lt_one,
le_iff_eq_or_lt, or_imp_distrib] {contextual := tt},
exact assume h₁ h₂,
⟨assume eq, by rw [eq] at h₂; exact (lt_irrefl _ h₂).elim,
assume h₃, (lt_irrefl a' $ lt_trans h₂ h₃).elim⟩
end,
calc lebesgue {a} = lebesgue (Ico a (a + 1) \ Ioo a (a + 1)) :
congr_arg _ this.symm
... = lebesgue (Ico a (a + 1)) - lebesgue (Ioo a (a + 1)) :
measure_sdiff (assume x, and.imp le_of_lt id) is_measurable_Ico is_measurable_Ioo $
by simp [lebesgue_Ico]; exact ennreal.of_real_lt_infty
... = 0 : by simp [lebesgue_Ico, lebesgue_Ioo]
by rw [← Ico_sdiff_Ioo_eq_singleton (lt_add_one a),
@measure_sdiff ℝ _ _ _ _ Ioo_subset_Ico_self is_measurable_Ico is_measurable_Ioo];
simp; exact ennreal.of_real_lt_infty

end measure_theory
10 changes: 9 additions & 1 deletion analysis/measure_theory/outer_measure.lean
View file
Expand Up @@ -166,7 +166,7 @@ have is_sum (λi, ε' i) ε, begin rw [eq] at this, exact this end,
ennreal.tsum_of_real this (assume i, le_of_lt $ hε' i)

/-- Given any function `m` assigning measures to sets satisying `m ∅ = 0`, there is
a unique minimal outer measure `μ` satisfying `μ s ≥ m s` for all `s : set α`. -/
a unique maximal outer measure `μ` satisfying `μ s ≤ m s` for all `s : set α`. -/
protected def of_function {α : Type*} (m : set α → ennreal) (m_empty : m ∅ = 0) :
outer_measure α :=
let μ := λs, ⨅{f : ℕ → set α} (h : s ⊆ ⋃i, f i), ∑i, m (f i) in
Expand Down Expand Up @@ -208,6 +208,14 @@ let μ := λs, ⨅{f : ℕ → set α} (h : s ⊆ ⋃i, f i), ∑i, m (f i) in
show μ (⋃ (i : ℕ), s i) ≤ (∑ (i : ℕ), μ (s i)) + of_real ε,
from infi_le_of_le f' $ infi_le_of_le hf' $ this }

theorem of_function_le {α : Type*} (m : set α → ennreal) (m_empty s) :
(outer_measure.of_function m m_empty).measure_of s ≤ m s :=
let f : ℕ → set α := λi, nat.rec_on i s (λn s, ∅) in
infi_le_of_le f $ infi_le_of_le (subset_Union f 0) $ le_of_eq $
calc (∑i, m (f i)) = ({0} : finset ℕ).sum (λi, m (f i)) :
tsum_eq_sum $ by intro i; cases i; simp [m_empty]
... = m s : by simp; refl

end of_function

section caratheodory_measurable
Expand Down
2 changes: 1 addition & 1 deletion analysis/topology/topological_structures.lean
View file
Expand Up @@ -765,7 +765,7 @@ begin
{ have h : {b | abs (a + -b) < r} = {b | a - r < b} ∩ {b | b < a + r},
from set.ext (assume b,
by simp [abs_lt, -sub_eq_add_neg, (sub_eq_add_neg _ _).symm,
sub_lt, lt_sub_iff, and_comm, sub_lt_iff_lt_add']),
sub_lt, lt_sub_iff_add_lt, and_comm, sub_lt_iff_lt_add']),
rw [h, ← inf_principal],
apply le_inf _ _,
{ exact infi_le_of_le {b : α | a - r < b} (infi_le_of_le (sub_lt_self a hr) $
Expand Down
2 changes: 1 addition & 1 deletion data/int/basic.lean
View file
Expand Up @@ -80,7 +80,7 @@ sub_lt_iff_lt_add.trans lt_add_one_iff
theorem le_sub_one_iff {a b : ℤ} : a ≤ b - 1 ↔ a < b :=
le_sub_iff_add_le

protected lemma induction_on {p : ℤ → Prop}
@[elab_as_eliminator] protected lemma induction_on {p : ℤ → Prop}
(i : ℤ) (hz : p 0) (hp : ∀i, p i → p (i + 1)) (hn : ∀i, p i → p (i - 1)) : p i :=
begin
induction i,
Expand Down
22 changes: 22 additions & 0 deletions data/set/intervals.lean
View file
Expand Up @@ -49,6 +49,8 @@ by rw ← not_lt; exact

@[simp] lemma Ico_eq_empty : b ≤ a → Ico a b = ∅ := Ico_eq_empty_iff.mpr

lemma Ico_self : Ico a a = ∅ := Ico_eq_empty $ le_refl _

lemma Ico_subset_Ico_iff (h₁ : a₁ < b₁) : Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ (a₂ ≤ a₁ ∧ b₁ ≤ b₂) :=
⟨assume h,
have h' : a₁ ∈ Ico a₂ b₂, from h ⟨le_refl _, h₁⟩,
Expand All @@ -58,6 +60,26 @@ lemma Ico_subset_Ico_iff (h₁ : a₁ < b₁) : Ico a₁ b₁ ⊆ Ico a₂ b₂
⟨h'.left, not_lt.1 $ this⟩,
assume ⟨h₁, h₂⟩ x ⟨hx₁, hx₂⟩, ⟨le_trans h₁ hx₁, lt_of_lt_of_le hx₂ h₂⟩⟩

lemma Ico_subset_Ico_left (h₁ : a₁ ≤ a₂) : Ico a₂ b ⊆ Ico a₁ b :=
λ c, and.imp_left $ le_trans h₁

lemma Ico_subset_Ico_right (h₁ : b₁ ≤ b₂) : Ico a b₁ ⊆ Ico a b₂ :=
λ c, and.imp_right $ λ h₂, lt_of_lt_of_le h₂ h₁

lemma Ico_subset_Ioo_left (h₁ : a₁ < a₂) : Ico a₂ b ⊆ Ioo a₁ b :=
λ c, and.imp_left $ lt_of_lt_of_le h₁

lemma Ioo_subset_Ico_self : Ioo a b ⊆ Ico a b := λ c, and.imp_left le_of_lt

lemma Ico_subset_Iio_self : Ioo a b ⊆ Iio b := λ c, and.right

lemma Ioo_self : Ioo a a = ∅ := subset_eq_empty Ioo_subset_Ico_self Ico_self

lemma Ico_sdiff_Ioo_eq_singleton (h : a < b) : Ico a b \ Ioo a b = {a} :=
set.ext $ λ c, by simp [Ioo, Ico, -not_lt]; exact
⟨λ ⟨⟨ac, cb⟩, h⟩, ((lt_or_eq_of_le ac).resolve_left $ λ hn, h hn cb).symm,
λ e, e.symm ▸ ⟨⟨le_refl _, h⟩, (lt_irrefl _).elim⟩⟩

lemma Ico_eq_Ico_iff : Ico a₁ b₁ = Ico a₂ b₂ ↔ ((b₁ ≤ a₁ ∧ b₂ ≤ a₂) ∨ (a₁ = a₂ ∧ b₁ = b₂)) :=
begin
cases lt_or_le a₁ b₁ with h₁ h₁; cases lt_or_le a₂ b₂ with h₂ h₂,
Expand Down

0 comments on commit 2d935cb

Please sign in to comment.