ι_injective — Mathlib

English

For each i, the map ι_i is injective.

Русский

Для каждого i отображение ι_i инъективно.

LaTeX

$$$\forall i, \text{Injective}(\iota_i)$$$

Lean4

theorem ι_injective (i : D.J) : Function.Injective (𝖣.ι i) :=
  by
  intro x y h
  rcases (D.ι_eq_iff_rel _ _ _ _).mp h with ⟨_, e₁, e₂⟩
  · dsimp only at *
        -- Porting note: there were `cases e₁` and `cases e₂`, instead of the `rw`

    rw [← e₁, ← e₂]
    simp

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