eq_of_mem_map_const — Mathlib

English

If b1 belongs to map (const α b2) l, then b1 = b2.

Русский

Если b1 принадлежит отображению константы b2 по списку l, то b1 = b2.

LaTeX

$$$\\\\forall {l:\\\\text{List }\\\\alpha},\\\\, b_1 \\\\in (\\\\operatorname{List.map} (\\\\operatorname{Function.const} \\\\alpha b_2) \\\\ l) \\\\Rightarrow b_1 = b_2.$$$

Lean4

theorem eq_of_mem_map_const {b₁ b₂ : β} {l : List α} (h : b₁ ∈ map (const α b₂) l) : b₁ = b₂ := by rw [map_const] at h;
  exact eq_of_mem_replicate h

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