emb_ne_emb_of_ne — Mathlib

English

If i ≠ j, then for any a and b, c.emb i a ≠ c.emb j b.

Русский

Если i ≠ j, то для любых a и b, c.emb i a ≠ c.emb j b.

LaTeX

$$$\\forall i,j:\\mathrm{Fin}(c.length),\\ i \\neq j \\Rightarrow \\forall a,b:\\mathrm{Fin}(c.partSize i)\\to\\mathrm{...},\\; c.emb i a \\neq c.emb j b$$$

Lean4

theorem emb_ne_emb_of_ne {i j : Fin c.length} {a : Fin (c.partSize i)} {b : Fin (c.partSize j)} (h : i ≠ j) :
    c.emb i a ≠ c.emb j b :=
  c.emb_injective.ne (a₁ := ⟨i, a⟩) (a₂ := ⟨j, b⟩) (by simp [h])

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