lift_injective — Mathlib

English

If each g_i is injective and the system is directed, the universal lift is injective.

Русский

Если каждый g_i инъективен и система направленная, то канонический взвод инъективен.

LaTeX

$$$\\text{lift\_inj}$: injective\\_condition $\\Rightarrow$ $\\text{lift}$ is injective$$

Lean4

theorem lift_injective [IsDirected ι (· ≤ ·)] (injective : ∀ i, Function.Injective <| g i) :
    Function.Injective (lift R ι G f g Hg) := by
  cases isEmpty_or_nonempty ι
  · apply Function.injective_of_subsingleton
  intro z w eq
  obtain ⟨i, x, y, rfl, rfl⟩ := exists_of₂ z w
  simp_rw [lift_of] at eq
  rw [injective _ eq]

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