mem_map_of_injective — Mathlib

English

If f is injective, then a ∈ map f l is equivalent to f a ∈ l.

Русский

Если f инъективна, то a входит в map f l тогда и только тогда, когда f a входит в l.

LaTeX

$$Injective f → (f a ∈ map f l) ↔ (a ∈ l)$$

Lean4

@[simp 1100, nolint simpNF]
theorem mem_map_of_injective {f : α → β} (H : Injective f) {a : α} {l : List α} : f a ∈ map f l ↔ a ∈ l :=
  ⟨fun m =>
    let ⟨_, m', e⟩ := exists_of_mem_map m;
    H e ▸ m',
    mem_map_of_mem⟩

Похожие утверждения