Skip to content

Commit

Permalink
fix
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Jul 27, 2024
1 parent a3eac33 commit ff6dcae
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Data/List/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -202,7 +202,7 @@ alias ⟨eq_nil_of_subset_nil, _⟩ := subset_nil

theorem map_subset_iff {l₁ l₂ : List α} (f : α → β) (h : Injective f) :
map f l₁ ⊆ map f l₂ ↔ l₁ ⊆ l₂ := by
refine ⟨?_, map_subset f⟩; intro h2 x hx
refine ⟨?_, Subset.map f⟩; intro h2 x hx
rcases mem_map.1 (h2 (mem_map_of_mem f hx)) with ⟨x', hx', hxx'⟩
cases h hxx'; exact hx'

Expand Down

0 comments on commit ff6dcae

Please sign in to comment.