Skip to content

Commit

Permalink
chore: correct List.Subset lemma names (#4843)
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em authored Jul 26, 2024
1 parent cbe39dc commit 18ba5f2
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions src/Init/Data/List/Lemmas.lean
Original file line number Diff line number Diff line change
Expand Up @@ -2574,13 +2574,13 @@ theorem cons_subset_cons {l₁ l₂ : List α} (a : α) (s : l₁ ⊆ l₂) : a
@[simp] theorem subset_nil {l : List α} : l ⊆ [] ↔ l = [] :=
fun h => match l with | [] => rfl | _::_ => (nomatch h (.head ..)), fun | rfl => Subset.refl _⟩

theorem map_subset {l₁ l₂ : List α} (f : α → β) (H : l₁ ⊆ l₂) : map f l₁ ⊆ map f l₂ :=
theorem Subset.map {l₁ l₂ : List α} (f : α → β) (H : l₁ ⊆ l₂) : map f l₁ ⊆ map f l₂ :=
fun x => by simp only [mem_map]; exact .imp fun a => .imp_left (@H _)

theorem filter_subset {l₁ l₂ : List α} (p : α → Bool) (H : l₁ ⊆ l₂) : filter p l₁ ⊆ filter p l₂ :=
theorem Subset.filter {l₁ l₂ : List α} (p : α → Bool) (H : l₁ ⊆ l₂) : filter p l₁ ⊆ filter p l₂ :=
fun x => by simp_all [mem_filter, subset_def.1 H]

theorem filterMap_subset {l₁ l₂ : List α} (f : α → Option β) (H : l₁ ⊆ l₂) :
theorem Subset.filterMap {l₁ l₂ : List α} (f : α → Option β) (H : l₁ ⊆ l₂) :
filterMap f l₁ ⊆ filterMap f l₂ := by
intro x
simp only [mem_filterMap]
Expand Down

0 comments on commit 18ba5f2

Please sign in to comment.