map_subset_iff — Mathlib

English

For an injective function f, map f l1 ⊆ map f l2 if and only if l1 ⊆ l2.

Русский

Для инъективной функции f имеют место: map f l1 ⊆ map f l2 тогда и только тогда, когда l1 ⊆ l2.

LaTeX

$$$$\\forall f:\\\\alpha \\\\to \\\\beta,\\ \\, Injective f \\\\rightarrow \\\\big( List.map f\, l_1 \\subseteq List.map f\, l_2 \\big) \\\\iff l_1 \\subseteq l_2.$$$$

Lean4

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
  rcases mem_map.1 (h2 (mem_map_of_mem hx)) with ⟨x', hx', hxx'⟩
  cases h hxx'; exact hx'

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