Plain-language statement
NB. Copied from Mathlib
Exact Lean statement
theorem inj_on_of_nodup_map {f : α → β} {l : List α} (d : List.Nodup (List.map f l)) :
∀ ⦃x⦄, x ∈ l → ∀ ⦃y⦄, y ∈ l → f x = f y → x = yFormal artifact
Lean source
theorem inj_on_of_nodup_map {f : α → β} {l : List α} (d : List.Nodup (List.map f l)) : ∀ ⦃x⦄, x ∈ l → ∀ ⦃y⦄, y ∈ l → f x = f y → x = y := by induction l with | nil => simp | cons hd tl ih => simp only [List.map, List.nodup_cons, List.mem_map, not_exists, not_and, ← Ne.eq_def] at d simp only [List.mem_cons] rintro _ (rfl | h₁) _ (rfl | h₂) h₃ · rfl · apply (d.1 _ h₂ h₃.symm).elim · apply (d.1 _ h₁ h₃).elim · apply ih d.2 h₁ h₂ h₃- Project
- Iris-Lean
- License
- Apache-2.0
- Commit
- 37f53e0ac065
- Source
- Iris/Iris/Std/FromMathlib.lean:31-42
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Co Pset Raw eq
CoPset.coPsetRaw_eq
Plain-language statement
Two CoPsetRaw trees are equal if they have the same membership function and both are well-formed.
Source project: Iris-Lean
Person-level attribution pending.
Big Op L hom weak
Iris.Algebra.BigOpL.bigOpL_hom_weak
Plain-language statement
Weak monoid homomorphisms distribute over non-empty big ops.
Source project: Iris-Lean
Person-level attribution pending.
Embed internal inj
Iris.BI.embed_internal_inj
Plain-language statement
⎡·⎤ reflects internal equality.
Source project: Iris-Lean
Person-level attribution pending.