image_mem_map_iff — Mathlib

English

If m is injective, then for any set s, m '' s ∈ map m f if and only if s ∈ f.

Русский

Если m инъективна, то для любого множества s выполнено: m''s ∈ map m f тогда и только если s ∈ f.

LaTeX

$$Injective m → (m''s ∈ map m f ↔ s ∈ f)$$

Lean4

@[simp 1100, nolint simpNF]
theorem image_mem_map_iff (hf : Injective m) : m '' s ∈ map m f ↔ s ∈ f :=
  ⟨fun h => by rwa [← preimage_image_eq s hf], image_mem_map⟩

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