map_injective — Mathlib

English

If φ is injective, then the map operation on variable changes is injective; distinct inputs give distinct outputs.

Русский

Если φ инъективна, то отображение переменных инъективно; разные входы дают разные выходы.

LaTeX

$$$$ \text{If }\varphi\text{ is injective, then }\text{map}(\varphi)\text{ is injective on the variable changes: }\forall C_1,C_2, \text{map}_{\varphi}(C_1) = \text{map}_{\varphi}(C_2) \Rightarrow C_1=C_2. $$$$

Lean4

theorem map_injective {φ : R →+* A} (hφ : Function.Injective φ) : Function.Injective <| map (φ := φ) := fun _ _ h =>
  by
  rcases mk.inj h with ⟨h, _, _, _⟩
  replace h := (Units.mk.inj h).left
  ext <;> apply_fun _ using hφ <;> assumption

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