lift_injective_iff — Mathlib

English

Injectivity of the lift corresponds to pointwise equality condition via g.

Русский

Инъективность лифта эквивалентна условию по точкам через g.

LaTeX

$$$ \\operatorname{Injective}(f.lift\\; hg) \\iff \\forall x,y,\\ f x = f y \\iff g x = g y $$$

Lean4

@[to_additive]
theorem lift_injective_iff : Function.Injective (f.lift hg) ↔ ∀ x y, f x = f y ↔ g x = g y :=
  by
  constructor
  · intro H x y
    constructor
    · exact f.eq_of_eq hg
    · intro h
      rw [← f.lift_eq hg, ← f.lift_eq hg] at h
      exact H h
  · intro H z w h
    obtain ⟨_, _⟩ := f.surj z
    obtain ⟨_, _⟩ := f.surj w
    rw [← f.mk'_sec z, ← f.mk'_sec w]
    exact (mul_inv f.map_units).2 ((H _ _).2 <| (mul_inv hg).1 h)

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