orderHom_injective — Mathlib

English

If f is injective, then orderHom f is injective.

Русский

Если f инъективно, то orderHom f инъективно.

LaTeX

$$$\\text{If } f \\text{ is injective, then } \\operatorname{orderHom} f \\text{ is injective}$$$

Lean4

@[to_additive]
theorem orderHom_injective {f : M →*o N} (h : Function.Injective f) : Function.Injective (orderHom f) :=
  by
  intro a b
  induction a using ind with
  | mk a
  induction b using ind with
  | mk b
  simp_rw [orderHom_mk, mk_eq_mk, ← map_mabs, ← map_pow]
  obtain hmono := (OrderHomClass.monotone f).strictMono_of_injective h
  intro ⟨⟨m, hm⟩, ⟨n, hn⟩⟩
  exact ⟨⟨m, hmono.le_iff_le.mp hm⟩, ⟨n, hmono.le_iff_le.mp hn⟩⟩

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