cons_injective — Mathlib

English

If a is not in s, then Pi.cons is injective on the family f: a ↦ δ a.

Русский

Если a не принадлежит s, то Pi.cons инъективна по f.

LaTeX

$$$\\text{If } a \\notin s,\\; \\mathrm{Injective}(\\mathrm{Pi.cons}\\ s\\ a\\ b).$$$

Lean4

theorem cons_injective {a : α} {b : δ a} {s : Multiset α} (hs : a ∉ s) : Function.Injective (Pi.cons s a b) :=
  fun f₁ f₂ eq =>
  funext fun a' =>
    funext fun h' =>
      have ne : a ≠ a' := fun h => hs <| h.symm ▸ h'
      have : a' ∈ a ::ₘ s := mem_cons_of_mem h'
      calc
        f₁ a' h' = Pi.cons s a b f₁ a' this := by rw [Pi.cons_ne this ne.symm]
        _ = Pi.cons s a b f₂ a' this := by rw [eq]
        _ = f₂ a' h' := by rw [Pi.cons_ne this ne.symm]

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