Skip to content

Commit

Permalink
fix(data/set/intervals/basic): fix a typo (#3680)
Browse files Browse the repository at this point in the history
  • Loading branch information
urkud committed Aug 3, 2020
1 parent 234011d commit b215e95
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/data/set/intervals/basic.lean
Expand Up @@ -557,13 +557,13 @@ subset.antisymm (λ x hx, hx.elim (λ hx, lt_of_le_of_lt hx h) and.right) Iio_su

variable {c : α}

lemma Ioo_subset_Ioo_union_Ici : Ioo a c ⊆ Ioo a b ∪ Ico b c :=
lemma Ioo_subset_Ioo_union_Ico : Ioo a c ⊆ Ioo a b ∪ Ico b c :=
λ x hx, (lt_or_le x b).elim (λ hxb, or.inl ⟨hx.1, hxb⟩) (λ hxb, or.inr ⟨hxb, hx.2⟩)

@[simp] lemma Ioo_union_Ico_eq_Ioo (h₁ : a < b) (h₂ : b ≤ c) : Ioo a b ∪ Ico b c = Ioo a c :=
subset.antisymm
(λ x hx, hx.elim (λ hx, ⟨hx.1, lt_of_lt_of_le hx.2 h₂⟩) (λ hx, ⟨lt_of_lt_of_le h₁ hx.1, hx.2⟩))
Ioo_subset_Ioo_union_Ici
Ioo_subset_Ioo_union_Ico

lemma Ico_subset_Ico_union_Ico : Ico a c ⊆ Ico a b ∪ Ico b c :=
λ x hx, (lt_or_le x b).elim (λ hxb, or.inl ⟨hx.1, hxb⟩) (λ hxb, or.inr ⟨hxb, hx.2⟩)
Expand Down

0 comments on commit b215e95

Please sign in to comment.