emb_injective — Mathlib

English

The map p ↦ c.emb p.1 p.2 is injective from Σ m, Fin (c.partSize m) to Fin n.

Русский

Отображение p ↦ c.emb p.1 p.2 инъективно: из сигма-типа в Fin(n).

LaTeX

$$$\\operatorname{Injective}\\left(\\lambda p: \\Sigma m, \\mathrm{Fin}(c.partSize\\,m)\\; ,\\; c.emb p.1 p.2\\right)$$$

Lean4

theorem emb_injective : Injective (fun (p : Σ m, Fin (c.partSize m)) ↦ c.emb p.1 p.2) :=
  by
  rintro ⟨m, r⟩ ⟨m', r'⟩ (h : c.emb m r = c.emb m' r')
  have : m = m' := by
    contrapose! h
    have A : Disjoint (range (c.emb m)) (range (c.emb m')) := c.disjoint (mem_univ m) (mem_univ m') h
    apply disjoint_iff_forall_ne.1 A (mem_range_self r) (mem_range_self r')
  subst this
  simpa using (c.emb_strictMono m).injective h

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