Skip to content

Commit

Permalink
chore: fix binder explicitness in List.map_subset
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Jul 31, 2024
1 parent afe0b5a commit 65d84ea
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/Init/Data/List/Sublist.lean
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ 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 map_subset {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₂ :=
Expand Down

0 comments on commit 65d84ea

Please sign in to comment.