injective — Mathlib

English

An elementary embedding is injective on the underlying domain.

Русский

Элементарное вложение инъективно на базовой области.

LaTeX

$$$\text{injective}(f) : \forall x,y, f(x)=f(y) \Rightarrow x=y.$$$

Lean4

@[simp]
theorem injective (φ : M ↪ₑ[L] N) : Function.Injective φ :=
  by
  intro x y
  have h := φ.map_formula ((var 0).equal (var 1) : L.Formula (Fin 2)) fun i => if i = 0 then x else y
  rw [Formula.realize_equal, Formula.realize_equal] at h
  simp only [Term.realize, Fin.one_eq_zero_iff, if_true, Function.comp_apply] at h
  exact h.1

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