eq_of_mem_map_const — Mathlib

English

If b1 is in the image of the list l under the constant function to b2, then b1 equals b2.

Русский

Если b1 принадлежит образу map (const α b2) на список l, то b1 = b2.

LaTeX

$$$$ b_1 \\in \\operatorname{map}(\\operatorname{const} α b_2) l \\Rightarrow b_1 = b_2 $$$$

Lean4

theorem eq_of_mem_map_const {b₁ b₂ : β} {l : List α} (h : b₁ ∈ map (Function.const α b₂) l) : b₁ = b₂ :=
  eq_of_mem_replicate (n := card (l : Multiset α)) <| by rwa [map_const] at h

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